Maximally informative alternatives

This file defines the maximally informative member of a scale-indexed family of propositions P : α → Set W: IsMaxInf P x w holds when P x is true at w and entails every member of the family true at w, i.e. P x is the least element under ⊆ of the image of the true set {y | w ∈ P y}. The per-world reading IsLeast {y | w ∈ P y} x maps to it along a monotone P by mathlib's Monotone.map_isLeast, and along an antitone one by Antitone.map_isGreatest.

Main declarations

• IsMaxInf, HasMaxInf: the maximally informative alternative and its existence.
• hasMaxInf_iff_isGreatest, hasMaxInf_iff_isLeast: on a strictly antitone (monotone) family, the maximally informative degree is the greatest (least) true one.
• exhChain_iff_isMaxInf: exhaustifying a strictly antitone family against its stronger members is asserting the prejacent maximally informative.
• hasMaxInf_ge_over, isMaxInf_ge_over_iff: "at least d" always has a maximally informative degree, the true measure; hasMaxInf_le_over, isMaxInf_le_over_iff are the duals.
• not_hasMaxInf_gt_over, hasMaxInf_gt_over_nat: "more than d" has no maximally informative degree on a dense scale and has one on ℕ.

References

• D. Fox, Free choice and the theory of scalar implicatures (2007)
• [D. Fox and M. Hackl, The universal density of measurement (2006)][fox-hackl-2006]
• [S. Beck and H. Rullmann, A flexible approach to exhaustivity in questions (1999)][beck-rullmann-1999]
• [K. von Fintel, D. Fox and S. Iatridou, Definiteness as maximal informativeness (2014)][von-fintel-fox-iatridou-2014]
• [V. Rouillard, Maximal informativity accounts for the distribution of temporal in-adverbials (2026)][rouillard-2026]

def Alternatives.IsMaxInf {α : Type u_1} {W : Type u_2} (P : α → Set W) (x : α) (w : W) : Prop

P x is maximally informative at w: true at w, and the least under ⊆ among the members of the family true at w.

Equations

• Alternatives.IsMaxInf P x w = IsLeast (P '' {y : α | w ∈ P y}) (P x)

def Alternatives.HasMaxInf {α : Type u_1} {W : Type u_2} (P : α → Set W) (w : W) : Prop

The family has a maximally informative member at w.

Equations

• Alternatives.HasMaxInf P w = ∃ (x : α), Alternatives.IsMaxInf P x w

theorem Alternatives.isMaxInf_iff {α : Type u_1} {W : Type u_2} {P : α → Set W} {x : α} {w : W} : IsMaxInf P x w ↔ w ∈ P x ∧ ∀ (y : α), w ∈ P y → P x ⊆ P y

Strictly monotone families

theorem Alternatives.hasMaxInf_iff_isGreatest {α : Type u_1} {W : Type u_2} [LinearOrder α] {φ : α → Set W} {w : W} (hφ : StrictAnti φ) : HasMaxInf φ w ↔ ∃ (m : α), IsGreatest {d : α | w ∈ φ d} m

On a strictly antitone family, a maximally informative degree is a greatest true degree.

theorem Alternatives.hasMaxInf_iff_isLeast {α : Type u_1} {W : Type u_2} [LinearOrder α] {φ : α → Set W} {w : W} (hφ : StrictMono φ) : HasMaxInf φ w ↔ ∃ (m : α), IsLeast {d : α | w ∈ φ d} m

On a strictly monotone family, a maximally informative degree is a least true degree.

theorem Alternatives.exhChain_iff_isMaxInf {α : Type u_1} {W : Type u_2} [LinearOrder α] {φ : α → Set W} {w : W} (hφ : StrictAnti φ) {i : α} : Exhaustification.exhChain φ i w ↔ IsMaxInf φ i w

Exhaustifying a strictly antitone family against all stronger members asserts that the prejacent is maximally informative.

Threshold properties

theorem Alternatives.hasMaxInf_ge_over {α : Type u_1} {W : Type u_2} [Preorder α] (μ : W → α) (w : W) : HasMaxInf (Degree.Comparison.ge.over μ) w

"At least d" is maximally informative at the true measure.

theorem Alternatives.isMaxInf_ge_over_iff {α : Type u_1} {W : Type u_2} [PartialOrder α] (μ : W → α) {m : α} (w : W) (hm : m ∈ Set.range μ) : IsMaxInf (Degree.Comparison.ge.over μ) m w ↔ μ w = m

The maximally informative "at least" degree is the true measure, whenever m is realized.

theorem Alternatives.not_hasMaxInf_gt_over {α : Type u_1} {W : Type u_2} [LinearOrder α] (μ : W → α) (w : W) [DenselyOrdered α] (hSurj : Function.Surjective μ) : ¬HasMaxInf (Degree.Comparison.gt.over μ) w

On a dense scale every degree of which is realized, "more than d" has no maximally informative degree ([fox-hackl-2006]).

theorem Alternatives.not_hasMaxInf_lt_over {α : Type u_1} {W : Type u_2} [LinearOrder α] (μ : W → α) (w : W) [DenselyOrdered α] (hSurj : Function.Surjective μ) : ¬HasMaxInf (Degree.Comparison.lt.over μ) w

On a dense scale every degree of which is realized, "less than d" has no maximally informative degree: not_hasMaxInf_gt_over on the dual scale.

theorem Alternatives.hasMaxInf_le_over {α : Type u_1} {W : Type u_2} [LinearOrder α] (μ : W → α) (w : W) : HasMaxInf (Degree.Comparison.le.over μ) w

"At most d" is maximally informative at the true measure: hasMaxInf_ge_over on the dual scale.

theorem Alternatives.isMaxInf_le_over_iff {α : Type u_1} {W : Type u_2} [LinearOrder α] (μ : W → α) {m : α} (w : W) (hm : m ∈ Set.range μ) : IsMaxInf (Degree.Comparison.le.over μ) m w ↔ μ w = m

The maximally informative "at most" degree is the true measure ([rouillard-2026]'s direction): isMaxInf_ge_over_iff on the dual scale.

theorem Alternatives.hasMaxInf_gt_over_nat {W : Type u_2} (μ : W → ℕ) (w : W) (hw : w ∈ Degree.Comparison.gt.over μ 0) : HasMaxInf (Degree.Comparison.gt.over μ) w

On ℕ, "more than d" has a maximally informative degree, μ w - 1: the discrete scale rescues what density forbids.