Measure extension

Formulation of Theorem 1 stating that:

A function μ : { B{b} | b.Finite } → [0,1] extends to a measure μ : ℬ → [0,1] under certain conditions.

The general outline of the proof of this theorem is as follows:

• First determining a finite b s.t. any B ∈ ℬ becomes a B ∈ ℬ{b}.
  • The b is given by ProbNetKAT.ℬ_b_mem_iff_exists.
  • The extension here is done by Carathéodory's extension theorem, given by MeasureTheory.AddContent.measure.
• The measure μ B of any such B can be written as the finite disjoint union of atoms (see ProbNetKAT.ℬ_b_exists_decomposition), giving us ∑ a, μ A{a,b}.
• The measure μ A{a,b} can be further decomposed using inclusion-exclusion (see MeasureTheory.ennreal_inclusion_exclusion). This then becomes a sum over B{b} by ProbNetKAT.B_b_union_eq_inter.

Connecting the steps defines a new measure on ℬ defined only on B{b} for finite b.

theorem ProbNetKAT.asdadss {H : Type} {b : Set H} {B : Set (Set H)} (μ : MeasureTheory.Measure (Set H)) (hb : b.Finite) (hB : B ∈ ℬ{b}) : ∃ (q : Set (Set H)), μ B = ∑' (a : ↑q), μ A{↑a,b}

theorem ProbNetKAT.asdadss' {H : Type} {B : Set (Set H)} (μ : MeasureTheory.Measure (Set H)) (hB : B ∈ ℬ{Set.univ}) : ∃ (b : Set H) (q : Set (Set H)), μ B = ∑' (a : ↑q), μ A{↑a,b}

def ProbNetKAT.B_b_fin {H : Type} : Set (Set (Set H))

The set of all B{b} generated by b finite.

Equations

• ProbNetKAT.B_b_fin = (fun (x : Set H) => B{x}) '' {b : Set H | b.Finite}

noncomputable instance ProbNetKAT.instFintypeElemSetSetOfAndSubset_probNetKAT {H : Type} {a b : Set H} (hb : b.Finite) : Fintype ↑{c : Set H | a ⊆ c ∧ c ⊆ b}

Equations

• ProbNetKAT.instFintypeElemSetSetOfAndSubset_probNetKAT hb = id (let_fun this := ⋯; let_fun this := this; Fintype.ofFinite { c : Set H // a ⊆ c ∧ c ⊆ b })

noncomputable def ProbNetKAT.mid_set {H : Type} {a b : Finset H} (hab : a ⊆ b) : Finset (Finset H)

Equations

• ProbNetKAT.mid_set hab = {c : Finset H | a ⊆ c ∧ c ⊆ b}.toFinset

@[simp]

theorem ProbNetKAT.mid_set_mem_iff {H : Type} {c a b : Finset H} {hab : a ⊆ b} : c ∈ mid_set hab ↔ a ⊆ c ∧ c ⊆ b

@[simp]

theorem ProbNetKAT.mid_set_insert {H : Type} {w : H} {a b : Finset H} (hab : a ⊆ insert w b) : ↑(mid_set hab) = {c : Finset H | a ⊆ c ∧ c ⊆ b} ∪ (fun (x : Finset H) => insert w x) '' {c : Finset H | a ⊆ c ∧ c ⊆ b}

theorem ProbNetKAT.A_ab_inclusion_exclusion {H : Type} {a b : Finset H} (μ : Set (Set H) → ENNReal) (hab : a ⊆ b) : μ A{↑a,↑b} = (∑ c ∈ mid_set hab, if (c \ a).card % 2 = 0 then μ B{↑c} else 0) - ∑ c ∈ mid_set hab, if (c \ a).card % 2 = 1 then μ B{↑c} else 0

def ProbNetKAT.measure_of_fin_req {H : Type} (μ : ↑B_b_fin → ENNReal) : Prop

Equations

• ProbNetKAT.measure_of_fin_req μ = ∀ (a b : Finset H) (hab : a ⊆ b), 0 ≤ ∑' (c : { x : Finset H // x ∈ ProbNetKAT.mid_set hab }), 1 ^ sorry * μ ⟨B{↑↑c}, ⋯⟩

def ProbNetKAT.ℬ_b_pick {H : Type} (B : Set (Set H)) (h : B ∈ ℬ{Set.univ}) : Set H

Equations

• ProbNetKAT.ℬ_b_pick B h = ⋯.choose

def ProbNetKAT.ℬ_b_pick_spec {H : Type} (B : Set (Set H)) (h : B ∈ ℬ{Set.univ}) : (ℬ_b_pick B h).Finite ∧ B ∈ ℬ{ℬ_b_pick B h}

Equations

• ⋯ = ⋯

theorem ProbNetKAT.ℬ_b_decompsoe {H : Type} {b : Set H} {B : Set (Set H)} (hb : b.Finite) (hB : B ∈ ℬ{b}) : ∃ (A : Set (Set H)), (∀ a ∈ A, a ⊆ b) ∧ B = ⋃ a ∈ A, A{a,b}

def ProbNetKAT.ℬ_b_decompsoe_pick {H : Type} (b : Set H) (hb : b.Finite) (B : Set (Set H)) (hB : B ∈ ℬ{b}) : Set (Set H)

Equations

• ProbNetKAT.ℬ_b_decompsoe_pick b hb B hB = ⋯.choose

def ProbNetKAT.ℬ_b_decompsoe_pick_spec {H : Type} (b : Set H) (hb : b.Finite) (B : Set (Set H)) (hB : B ∈ ℬ{b}) : (∀ a ∈ ℬ_b_decompsoe_pick b hb B hB, a ⊆ b) ∧ B = ⋃ a ∈ ℬ_b_decompsoe_pick b hb B hB, A{a,b}

Equations

• ⋯ = ⋯

@[simp]

theorem ProbNetKAT.ℬ_b_decompsoe_pick_empty_is_empty {α✝ : Type} {b : Set α✝} {hb : b.Finite} : ℬ_b_decompsoe_pick b hb ∅ ⋯ = ∅

noncomputable def ProbNetKAT.extend_B_b_fin_A_ab {H : Type} (μ : ↑B_b_fin → ENNReal) (a b : Set H) (ha : a ⊆ b) : ENNReal

Extension to μ(A{a,b}) for a ⊆ b and finite b.

Equations

• ProbNetKAT.extend_B_b_fin_A_ab μ a b ha = ∑' (c : ↑{c : Set H | a ⊆ c ∧ c ⊆ b}), μ ⟨B{↑c}, ⋯⟩

noncomputable def ProbNetKAT.extend_B_b_fin {H : Type} (μ : ↑B_b_fin → ENNReal) (b : Set H) (hb : b.Finite) : ↑ℬ{b} → ENNReal

Extension to μ(B) where B ∈ ℬ{b} for finite b.

Equations

• ProbNetKAT.extend_B_b_fin μ b hb ⟨B, hB⟩ = ∑' (a : ↑(ProbNetKAT.ℬ_b_decompsoe_pick b hb B hB)), ProbNetKAT.extend_B_b_fin_A_ab μ (↑a) b ⋯

@[simp]

theorem ProbNetKAT.extend_B_b_fin_apply {H : Type} (μ : ↑B_b_fin → ENNReal) (b : Set H) (hb : b.Finite) (B : ↑ℬ{b}) : extend_B_b_fin μ b hb B = ∑' (a : ↑(ℬ_b_decompsoe_pick b hb ↑B ⋯)), extend_B_b_fin_A_ab μ (↑a) b ⋯

noncomputable def ProbNetKAT.extend_B_b_fin' {H : Type} (μ : ↑B_b_fin → ENNReal) : ↑ℬ{Set.univ} → ENNReal

Extension to μ(B) where B ∈ ℬ{Set.univ}.

Equations

• ProbNetKAT.extend_B_b_fin' μ ⟨B, hB⟩ = ProbNetKAT.extend_B_b_fin μ (ProbNetKAT.ℬ_b_pick B hB) ⋯ ⟨B, ⋯⟩

@[simp]

theorem ProbNetKAT.extend_B_b_fin_empty {H : Type} (μ : ↑B_b_fin → ENNReal) (b : Set H) (hb : b.Finite) : extend_B_b_fin μ b hb ⟨∅, ⋯⟩ = 0

@[simp]

theorem ProbNetKAT.extend_B_b_fin'_apply' {H : Type} (μ : ↑B_b_fin → ENNReal) (B : ↑ℬ{Set.univ}) : extend_B_b_fin' μ B = extend_B_b_fin μ (ℬ_b_pick ↑B ⋯) ⋯ ⟨↑B, ⋯⟩

noncomputable def ProbNetKAT.AddContent_ofFin {H : Type} (μ : ↑B_b_fin → ENNReal) (h : measure_of_fin_req μ) : MeasureTheory.AddContent ℬ{Set.univ}

Equations

• ProbNetKAT.AddContent_ofFin μ h = { toFun := fun (B : Set (Set H)) => if hB : B ∈ ℬ{Set.univ} then ProbNetKAT.extend_B_b_fin' μ ⟨B, hB⟩ else 0, empty' := ⋯, sUnion' := ⋯ }

theorem ProbNetKAT.AddContent_ofFin_IsSigmaSubadditive {α✝ : Type} {μ : ↑B_b_fin → ENNReal} {h : measure_of_fin_req μ} : (AddContent_ofFin μ h).IsSigmaSubadditive

noncomputable def ProbNetKAT.measure_of_fin {H : Type} (μ : ↑B_b_fin → ENNReal) (h : measure_of_fin_req μ) : MeasureTheory.Measure (Set H)

Theorem 1. A function μ : {B{b} | b finite} → [0, 1] extends to a measure μ : ℬ → [0, 1] iff for all finite b and all a ⊆ b

$$ ∑_{a ⊆ c ⊆ b} (-1)^{|c \ a|} μ(B\{c\}) ≥ 0 $$

Moreover, the extension to ℬ is unique.

Equations

• ProbNetKAT.measure_of_fin μ h = (ProbNetKAT.AddContent_ofFin μ h).measure ⋯ ⋯ ⋯