Aumann's agreement theorem

This file develops information partitions and conditional probabilities needed for Aumann's agreement theorem.

@[reducible, inline]

abbrev AgreeToDisagree.Partition (α : Type u_3) : Type u_3

We write Partition α for the type of partitions of a set α, implemented as a subtype of Set (Set α). Mathlib already equips this subtype with the order given by refinement (such that P ≤ Q iff P refines Q) and proves that it is a complete lattice, i.e. that arbitrary infima and suprema of partitions exist.

Equations

• AgreeToDisagree.Partition α = Setoid.Partitions α

@[reducible]

instance AgreeToDisagree.Partition.instSetLike {α : Type u_1} : SetLike (Partition α) (Set α)

When we write s ∈ P for a partition P : Partition α, we mean that s is a Set α that is an element of the Set (Set α) underlying P.

Equations

• AgreeToDisagree.Partition.instSetLike = { coe := Subtype.val, coe_injective := ⋯ }

theorem AgreeToDisagree.Partition.le_iff {α : Type u_1} {P Q : Partition α} : P ≤ Q ↔ ∀ s ∈ P, ∃ t ∈ Q, s ⊆ t

As expected, a partition P refines a partition Q iff every set in P is contained in a set in Q.

def AgreeToDisagree.Partition.Measurable {Ω : Type u_2} [MeasurableSpace Ω] (P : Partition Ω) : Prop

We call a partition of a measurable space measurable if it consists of measurable sets.

Equations

• P.Measurable = ∀ s ∈ P, MeasurableSet s

theorem AgreeToDisagree.Partition.Measurable.mono {Ω : Type u_2} [MeasurableSpace Ω] {P Q : Partition Ω} (hP : P.Measurable) (hP' : (↑P).Countable) (hQ : P ≤ Q) : Q.Measurable

If a countable partition is measurable, every partition it refines is measurable too. Note that the countability assumption is necessary because e.g. the partition into singletons is usually measurable but refines all other partitions, even nonmeasurable ones.

theorem AgreeToDisagree.Partition.Measurable.sup {Ω : Type u_2} [MeasurableSpace Ω] {P Q : Partition Ω} (hP : P.Measurable) (hQ : Q.Measurable) (h : (↑P).Countable ∨ (↑Q).Countable) : (P ⊔ Q).Measurable

The supremum of two measurable partitions is measurable if at least one of the two partitions is countable.

def AgreeToDisagree.Partition.class {α : Type u_1} (P : Partition α) (a : α) : Set α

P.class a is the element of a partition P : Partition α that contains a : α.

Equations

• P.class a = {b : α | (Setoid.mkClasses ↑P ⋯) b a}

theorem AgreeToDisagree.Partition.mem_class {α : Type u_1} (P : Partition α) (a : α) : a ∈ P.class a

theorem AgreeToDisagree.Partition.class_mem {α : Type u_1} (P : Partition α) (a : α) : P.class a ∈ P

theorem AgreeToDisagree.Partition.Measurable.measurableSet_class {Ω : Type u_2} [MeasurableSpace Ω] {P : Partition Ω} (hP : P.Measurable) (ω : Ω) : MeasurableSet (P.class ω)

theorem AgreeToDisagree.Partition.class_mono {α : Type u_1} {P Q : Partition α} (h : P ≤ Q) (a : α) : P.class a ⊆ Q.class a

theorem AgreeToDisagree.Partition.class_eq_class_of_mem {α : Type u_1} {P : Partition α} {a a' : α} (h : a' ∈ P.class a) : P.class a' = P.class a

theorem AgreeToDisagree.Partition.class_eq_of_mem {α : Type u_1} {P : Partition α} {s : Set α} {a : α} (hs : s ∈ P) (ha : a ∈ s) : P.class a = s

theorem AgreeToDisagree.Partition.class_eq_biUnion_of_le {α : Type u_1} {P Q : Partition α} (h : P ≤ Q) (a : α) : Q.class a = ⋃ s ∈ {s : Set α | s ∈ P ∧ s ⊆ Q.class a}, s

theorem AgreeToDisagree.Partition.class_subset_of_le {α : Type u_1} {P Q : Partition α} (hle : P ≤ Q) (ω : α) : P.class ω ⊆ Q.class ω

theorem AgreeToDisagree.Partition.class_eq_of_mem_part {α : Type u_1} {P : Partition α} {s : Set α} {ω : α} (hs : s ∈ P) (hω : ω ∈ s) : P.class ω = s

theorem AgreeToDisagree.Partition.pairwise_disjoint_subtype_val {α : Type u_1} (P : Partition α) : Pairwise (Function.onFun Disjoint fun (i : ↑↑P) => ↑i)

@[reducible, inline]

noncomputable abbrev AgreeToDisagree.Partition.probabilityAt {Ω : Type u_2} [MeasurableSpace Ω] (P : Partition Ω) (μ : MeasureTheory.Measure Ω) (E : Set Ω) (ω : Ω) : ENNReal

Conditional probability of an event inside the atom of a partition containing a point.

Equations

• P.probabilityAt μ E ω = μ (E ∩ P.class ω) / μ (P.class ω)

theorem AgreeToDisagree.Partition.countable_of_measure_pos {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P : Partition Ω} (hP : P.Measurable) (hP' : ∀ s ∈ P, μ s > 0) : (↑P).Countable

A partition with all parts of positive measure is countable.

theorem AgreeToDisagree.Partition.countable_of_pos_measure {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Partition Ω) (hP : P.Measurable) (hP' : ∀ s ∈ P, μ s > 0) : (↑P).Countable

theorem AgreeToDisagree.measure_inter_eq_mul_of_probabilityAt_eq {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Partition Ω) (hP' : ∀ s ∈ P, μ s > 0) {E s S : Set Ω} {p : ENNReal} (hs : s ∈ P) (hsS : s ⊆ S) (hconst : ∀ ω' ∈ S, P.probabilityAt μ E ω' = p) : μ (E ∩ s) = p * μ s

theorem AgreeToDisagree.measure_inter_sup_class_eq_mul {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Partition Ω) (hPm : P.Measurable) (hP' : ∀ s ∈ P, μ s > 0) {E S : Set Ω} {p : ENNReal} (hE : MeasurableSet E) (hS : S = ⋃ s ∈ {s : Set Ω | s ∈ P ∧ s ⊆ S}, s) (hctbl : (↑P).Countable) (hconst : ∀ ω' ∈ S, P.probabilityAt μ E ω' = p) : μ (E ∩ S) = p * μ S

theorem AgreeToDisagree.Partition.probabilityAt_eq_of_le {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P Q : Partition Ω} (hP : P.Measurable) (hP' : ∀ s ∈ P, μ s > 0) (hQ : P ≤ Q) {E : Set Ω} (hE : MeasurableSet E) (ω : Ω) {p : ENNReal} (h : ∀ ω' ∈ Q.class ω, P.probabilityAt μ E ω' = p) : Q.probabilityAt μ E ω = p

Let P be a partition of Ω into measurable non-null sets, Q a coarser partition and E a set such that P.probabilityAt E ω' = p for all ω' ∈ Q.class ω. Then Q.probabilityAt E ω = p.

theorem AgreeToDisagree.agreeToDisagree {Ω : Type u_2} [MeasurableSpace Ω] {μ₁ μ₂ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {P₁ P₂ : Partition Ω} (hP₁ : P₁.Measurable) (hP₂ : P₂.Measurable) (hP₁' : ∀ s ∈ P₁, μ₁ s > 0) (hP₂' : ∀ s ∈ P₂, μ₂ s > 0) {E : Set Ω} (hE : MeasurableSet E) (ω : Ω) {p₁ p₂ : ENNReal} (h : (P₁ ⊔ P₂).class ω ⊆ {ω' : Ω | P₁.probabilityAt μ₁ E ω' = p₁ ∧ P₂.probabilityAt μ₂ E ω' = p₂}) (h' : (P₁ ⊔ P₂).probabilityAt μ₁ E ω = (P₁ ⊔ P₂).probabilityAt μ₂ E ω) : p₁ = p₂

Let Ω be a probability measure space, P₁ and P₂ two measurable partitions representing the information partitions of two agents, E a measurable set and ω an event. Then if it is common knowledge at ω that E appears to have probability p₁ to the first agent and probability p₂ to the second agent, p₁ = p₂ - that is, the two agents agree on the probability of E.

theorem AgreeToDisagree.agreeToDisagree' {Ω : Type u_2} [MeasurableSpace Ω] {ι : Type u_3} {μ : ι → MeasureTheory.Measure Ω} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {P : ι → Partition Ω} (hP : ∀ (i : ι), (P i).Measurable) (hP' : ∀ (i : ι), ∀ s ∈ P i, (μ i) s > 0) {E : Set Ω} (hE : MeasurableSet E) (ω : Ω) {p : ι → ENNReal} (h : (⨆ (i : ι), P i).class ω ⊆ {ω' : Ω | ∀ (i : ι), (P i).probabilityAt (μ i) E ω' = p i}) (h' : ∀ (i j : ι), (⨆ (i : ι), P i).probabilityAt (μ i) E ω = (⨆ (i : ι), P i).probabilityAt (μ j) E ω) (i j : ι) : p i = p j

Let Ω be a probability measure space, P a family of measurable partitions representing the information partitions of agents indexed by a type ι, E a measurable set and ω an event. Then if it is common knowledge at ω that E appears to have probability p i to each agent i, p i = p j for all i, j - that is, all agents agree on the probability of E.