Approximate agreement under common belief

This file proves the p-belief version of Aumann's agreement theorem.

@[reducible, inline]

abbrev AgreeToDisagree.Partition.belief {Ω : Type u_1} [MeasurableSpace Ω] (P : Partition Ω) (μ : MeasureTheory.Measure Ω) (p : ENNReal) (E : Set Ω) : Set Ω

The set of states where the posterior probability of E is at least p.

Equations

• P.belief μ p E = {ω : Ω | p ≤ P.probabilityAt μ E ω}

@[reducible, inline]

abbrev AgreeToDisagree.Partition.IsEvidentBelief {Ω : Type u_1} [MeasurableSpace Ω] (P : Partition Ω) (μ : MeasureTheory.Measure Ω) (p : ENNReal) (E : Set Ω) : Prop

A set is p-evident for a partition if membership implies p-belief in itself.

Equations

• P.IsEvidentBelief μ p E = (E ⊆ P.belief μ p E)

@[reducible, inline]

abbrev AgreeToDisagree.IsCommonBeliefAt {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} (P : ι → Partition Ω) (μ : MeasureTheory.Measure Ω) (p : ENNReal) (C : Set Ω) (ω : Ω) : Prop

Common p-belief at a state, represented by an evident event containing that state.

Equations

• AgreeToDisagree.IsCommonBeliefAt P μ p C ω = ∃ (E : Set Ω), ω ∈ E ∧ (∀ (i : ι), (P i).IsEvidentBelief μ p E) ∧ ∀ (i : ι), E ⊆ (P i).belief μ p C

theorem AgreeToDisagree.Partition.belief_mono {Ω : Type u_1} [MeasurableSpace Ω] (P : Partition Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ENNReal) {X Y : Set Ω} (hXY : X ⊆ Y) : P.belief μ p X ⊆ P.belief μ p Y

Monotonicity of belief: X ⊆ Y implies P.belief μ p X ⊆ P.belief μ p Y.

theorem AgreeToDisagree.Partition.belief_eq_biUnion {Ω : Type u_1} [MeasurableSpace Ω] {P : Partition Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ENNReal) (X : Set Ω) : P.belief μ p X = ⋃ s ∈ {s : Set Ω | s ∈ P ∧ p ≤ μ (X ∩ s) / μ s}, s

The belief set equals a union over partition atoms with sufficient conditional probability.

theorem AgreeToDisagree.Partition.measurableSet_belief {Ω : Type u_1} [MeasurableSpace Ω] {P : Partition Ω} (hP : P.Measurable) (hPc : (↑P).Countable) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ENNReal) (X : Set Ω) : MeasurableSet (P.belief μ p X)

For a measurable countable partition P, the belief set P.belief μ p X is measurable.

theorem AgreeToDisagree.Partition.belief_belief_subset {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P : Partition Ω} {p : ENNReal} (hp : 0 < p) (X : Set Ω) : P.belief μ p (P.belief μ p X) ⊆ P.belief μ p X

The downward step of belief idempotence.

theorem AgreeToDisagree.ennreal_num_pos_of_ratio_ge {p a b : ENNReal} (hp : 0 < p) (h : p ≤ a / b) : 0 < a

If 0 < p ≤ a / b, then 0 < a.

theorem AgreeToDisagree.measure_pos_of_evident_belief {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {P : Partition Ω} {p : ENNReal} (hp : 0 < p) {A : Set Ω} {ω : Ω} (hω : ω ∈ A) (hev : A ⊆ P.belief μ p A) : 0 < μ A

If A is p-evident with 0 < p, then μ A > 0.

theorem AgreeToDisagree.nonempty_of_measure_pos {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s : Set Ω} (h : 0 < μ s) : s.Nonempty

A set of positive measure is nonempty.

theorem AgreeToDisagree.probabilityAt_eq_of_belief_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P : Partition Ω} {p : ENNReal} (hp : 0 < p) {E A : Set Ω} {r : ENNReal} (hA : A ⊆ P.belief μ p {ω : Ω | P.probabilityAt μ E ω = r}) (ω : Ω) : ω ∈ A → P.probabilityAt μ E ω = r

If A ⊆ P.belief μ p {ω | P.probabilityAt μ E ω = r}, then probability equals r on A.

Helpers for core_bound

theorem AgreeToDisagree.core_bound.atom_E_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P : Partition Ω} (hP' : ∀ s ∈ P, μ s > 0) {A E : Set Ω} {r : ENNReal} (hAR : ∀ ω ∈ A, P.probabilityAt μ E ω = r) {s : Set Ω} (hs : s ∈ P) {ω : Ω} (hω : ω ∈ A ∩ s) : μ (E ∩ s) = r * μ s

theorem AgreeToDisagree.core_bound.atom_evidence {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P : Partition Ω} (hP' : ∀ s ∈ P, μ s > 0) {p : ENNReal} {A : Set Ω} (hAev : A ⊆ P.belief μ p A) {s : Set Ω} (hs : s ∈ P) {ω : Ω} (hω : ω ∈ A ∩ s) : p * μ s ≤ μ (A ∩ s)

theorem AgreeToDisagree.core_bound.atom_real_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P : Partition Ω} (hP' : ∀ s ∈ P, μ s > 0) {p : ENNReal} {A E : Set Ω} (hA : MeasurableSet A) {r : ENNReal} {s : Set Ω} (hs : s ∈ P) (hAsmu : 0 < μ (A ∩ s)) (hEs : μ (E ∩ s) = r * μ s) (hαs : p * μ s ≤ μ (A ∩ s)) : |(μ (E ∩ A ∩ s) / μ (A ∩ s)).toReal - r.toReal| ≤ 1 - p.toReal

theorem AgreeToDisagree.core_bound.tsum_decomp_A {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P : Partition Ω} (hP : P.Measurable) (hP' : ∀ s ∈ P, μ s > 0) {A : Set Ω} (hA : MeasurableSet A) : μ A = ∑' (s : ↑↑P), μ (A ∩ ↑s)

theorem AgreeToDisagree.core_bound.abs_sub_div_le_of_mul {T q r b : ℝ} (hT : 0 < T) (h : |r * T - q| ≤ T * b) : |r - q / T| ≤ b

theorem AgreeToDisagree.core_bound.weighted_atom_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P : Partition Ω} {A E : Set Ω} {p r : ENNReal} (hAtom : ∀ (s : ↑↑P), 0 < μ (A ∩ ↑s) → |(μ (E ∩ A ∩ ↑s) / μ (A ∩ ↑s)).toReal - r.toReal| ≤ 1 - p.toReal) (s : ↑↑P) : |(μ (A ∩ ↑s)).toReal * r.toReal - (μ (E ∩ A ∩ ↑s)).toReal| ≤ (μ (A ∩ ↑s)).toReal * (1 - p.toReal)

theorem AgreeToDisagree.core_bound.weighted_sum_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P : Partition Ω} {p : ENNReal} {A E : Set Ω} {r : ENNReal} (hμA : μ A = ∑' (s : ↑↑P), μ (A ∩ ↑s)) (hμEA : μ (E ∩ A) = ∑' (s : ↑↑P), μ (E ∩ A ∩ ↑s)) (hAtom : ∀ (s : ↑↑P), 0 < μ (A ∩ ↑s) → |(μ (E ∩ A ∩ ↑s) / μ (A ∩ ↑s)).toReal - r.toReal| ≤ 1 - p.toReal) : |r.toReal * (μ A).toReal - (μ (E ∩ A)).toReal| ≤ (μ A).toReal * (1 - p.toReal)

theorem AgreeToDisagree.core_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P : Partition Ω} (hP : P.Measurable) (hP' : ∀ s ∈ P, μ s > 0) {p : ENNReal} {A E : Set Ω} (hA : MeasurableSet A) (hAmu : 0 < μ A) (hAev : A ⊆ P.belief μ p A) (hE : MeasurableSet E) {r : ENNReal} (hAR : ∀ ω ∈ A, P.probabilityAt μ E ω = r) : |r.toReal - (μ (E ∩ A) / μ A).toReal| ≤ 1 - p.toReal

Core bound (Step 4 of the informal proof).

theorem AgreeToDisagree.agreeToDisagree_beliefs {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {P : ι → Partition Ω} (hP : ∀ (i : ι), (P i).Measurable) (hP' : ∀ (i : ι), ∀ s ∈ P i, μ s > 0) {E : Set Ω} (hE : MeasurableSet E) (ω : Ω) {p : ENNReal} (hp : 0 < p) {r : ι → ENNReal} (h : IsCommonBeliefAt P μ p {ω : Ω | ∀ (i : ι), (P i).probabilityAt μ E ω = r i} ω) (i j : ι) : |(r i).toReal - (r j).toReal| ≤ 2 * (1 - p.toReal)