Mathlib extensions used by ProbNetKAT

These are general definitions and theorems unrelated but necessary for the ProbNetKAT formalization.

Main definitions

• Finset.nepowerset: A variant of Finset.powerset which excludes ∅.
• Finset.strongerInduction: An induction principle on Finset where the induction hypothesis can be applied to any finset with a smaller cardinality.
• Real.inclusion_exclusion: Inclusion-exclusion principle for real valued functions.
• MeasureTheory.real_inclusion_exclusion: Inclusion-exclusion principle for real valued measures.
• MeasureTheory.ennreal_inclusion_exclusion: Inclusion-exclusion principle for measures by way of reals.
• MeasureTheory.ennreal_inclusion_exclusion_even_odd: Inclusion-exclusion principle for measures expressed as the difference between the odd and the even terms.

Finset.nepowerset

def Finset.nepowerset {α : Type} [DecidableEq α] (s : Finset α) : Finset (Finset α)

Equations

• s.nepowerset = s.powerset \ {∅}

theorem Finset.nepowerset_eq {α : Type} [DecidableEq α] (s : Finset α) : s.nepowerset = s.powerset \ {∅}

theorem Finset.powerset_eq_empty_union_nepowerset {α : Type} [DecidableEq α] (s : Finset α) : s.powerset = {∅} ∪ s.nepowerset

@[simp]

theorem Finset.nepowerset_empty {α : Type} [DecidableEq α] : ∅.nepowerset = ∅

@[simp]

theorem Finset.nepowerset_singleton {α : Type} [DecidableEq α] {a : α} : {a}.nepowerset = {{a}}

@[simp]

theorem Finset.mem_nepowerset_iff {α : Type} [DecidableEq α] (s : Finset α) {x : Finset α} : x ∈ s.nepowerset ↔ x ⊆ s ∧ x ≠ ∅

theorem Finset.nepowerset_insert {α : Type} [DecidableEq α] (s : Finset α) {a : α} : (insert a s).nepowerset = s.nepowerset ∪ image (fun (x : Finset α) => insert a x) s.powerset

@[simp]

theorem Finset.nepowerset_pair {α : Type} [DecidableEq α] {a b : α} : {a, b}.nepowerset = {{a}, {b}, {a, b}}

theorem Finset.sum_nepowerset_insert {α : Type} [DecidableEq α] (s : Finset α) {β : Type u_1} {a : α} [AddCommMonoid β] (ha : a ∉ s) (f : Finset α → β) : ∑ t ∈ (insert a s).nepowerset, f t = ∑ t ∈ s.nepowerset, f t + ∑ t ∈ s.powerset, f (insert a t)

Finset.strongerInduction

def Finset.strongerInduction {α : Type u_1} {p : Finset α → Prop} (H : ∀ (s : Finset α), (∀ (t : Finset α), t.card < s.card → p t) → p s) (s : Finset α) : p s

Equations

• ⋯ = ⋯

def Finset.caseStrongerInduction {α : Type} [DecidableEq α] {p : Finset α → Prop} (h₀ : p ∅) (h₁ : ∀ (a : α) (s : Finset α), a ∉ s → (∀ (t : Finset α), t.card ≤ s.card → p t) → p (insert a s)) (s : Finset α) : p s

Equations

• ⋯ = ⋯

Inclusion-exclusion

theorem Real.inclusion_exclusion' {H : Type} [DecidableEq (Set (Set H))] (μ : Set (Set H) → ℝ) (I : Finset (Set (Set H))) (f : Set (Set H) → Set (Set H)) (hf : ∀ (a b : Set (Set H)), f (a ∩ b) = f a ∩ f b) (h₀ : μ ∅ = 0) (h₁ : ∀ (a b : Set (Set H)), μ (a ∪ b) = μ a + μ b - μ (a ∩ b)) : μ (⋃ c ∈ I, f c) = ∑ c ∈ I.nepowerset, (-1) ^ (c.card + 1) * μ (f (⋂₀ ↑c))

theorem Real.inclusion_exclusion {H : Type} [DecidableEq (Set (Set H))] (μ : Set (Set H) → ℝ) (I : Finset (Set (Set H))) (h₀ : μ ∅ = 0) (h₁ : ∀ (a b : Set (Set H)), μ (a ∪ b) = μ a + μ b - μ (a ∩ b)) : μ (⋃₀ ↑I) = ∑ c ∈ I.nepowerset, (-1) ^ (c.card + 1) * μ (⋂₀ ↑c)

theorem MeasureTheory.inclusion_exclusion₂ {H : Type u_1} {b a : Set (Set H)} (μ : Measure (Set H)) [IsFiniteMeasure μ] (h : MeasurableSet b) : μ (a ∪ b) = μ a + μ b - μ (a ∩ b)

theorem MeasureTheory.inclusion_exclusion₂_real {H : Type u_1} {b a : Set (Set H)} (μ : Measure (Set H)) [IsFiniteMeasure μ] (h : MeasurableSet b) : μ.real (a ∪ b) = μ.real a + μ.real b - μ.real (a ∩ b)

theorem MeasureTheory.real_inclusion_exclusion' {H : Type} [DecidableEq (Set (Set H))] (μ : Measure (Set H)) [IsFiniteMeasure μ] (I : Finset (Set (Set H))) (hI : ∀ i ∈ I, MeasurableSet i) (f : Set (Set H) → Set (Set H)) (hf : ∀ (a b : Set (Set H)), f (a ∩ b) = f a ∩ f b) (hfm : ∀ x ∈ I, MeasurableSet (f x)) : μ.real (⋃ c ∈ I, f c) = ∑ c ∈ I.nepowerset, (-1) ^ (c.card + 1) * μ.real (f (⋂₀ ↑c))

theorem MeasureTheory.real_inclusion_exclusion {H : Type} [DecidableEq (Set (Set H))] (μ : Measure (Set H)) [IsFiniteMeasure μ] (I : Finset (Set (Set H))) (hI : ∀ i ∈ I, MeasurableSet i) : μ.real (⋃₀ ↑I) = ∑ c ∈ I.nepowerset, (-1) ^ (c.card + 1) * μ.real (⋂₀ ↑c)

theorem MeasureTheory.real_inclusion_exclusion_even_odd {H : Type} [DecidableEq (Set (Set H))] (μ : Measure (Set H)) [IsFiniteMeasure μ] (I : Finset (Set (Set H))) : ∑ c ∈ I.nepowerset, (-1) ^ (c.card + 1) * μ.real (⋂₀ ↑c) = ∑ c ∈ I.nepowerset with Odd c.card, μ.real (⋂₀ ↑c) - ∑ c ∈ I.nepowerset with Even c.card, μ.real (⋂₀ ↑c)

theorem MeasureTheory.ennreal_inclusion_exclusion {H : Type} [DecidableEq (Set (Set H))] (μ : Measure (Set H)) [IsFiniteMeasure μ] (I : Finset (Set (Set H))) (hI : ∀ i ∈ I, MeasurableSet i) : μ (⋃₀ ↑I) = ENNReal.ofReal (∑ c ∈ I.nepowerset, (-1) ^ (c.card + 1) * μ.real (⋂₀ ↑c))

theorem MeasureTheory.probability_inclusion_exclusion {H : Type} [DecidableEq (Set (Set H))] (μ : ProbabilityMeasure (Set H)) (I : Finset (Set (Set H))) (hI : ∀ x ∈ I, MeasurableSet x) : μ (⋃₀ ↑I) = (∑ c ∈ I.nepowerset, (-1) ^ (c.card + 1) * ↑(μ (⋂₀ ↑c))).toNNReal

theorem MeasureTheory.ennreal_inclusion_exclusion_even_odd {H : Type} [DecidableEq (Set (Set H))] (μ : Measure (Set H)) [IsFiniteMeasure μ] (I : Finset (Set (Set H))) (hI : ∀ i ∈ I, MeasurableSet i) : μ (⋃₀ ↑I) = ∑ c ∈ I.nepowerset with Odd c.card, μ (⋂₀ ↑c) - ∑ c ∈ I.nepowerset with Even c.card, μ (⋂₀ ↑c)

theorem MeasureTheory.probability_inclusion_exclusion_even_odd {H : Type} [DecidableEq (Set (Set H))] (μ : ProbabilityMeasure (Set H)) (I : Finset (Set (Set H))) (hI : ∀ x ∈ I, MeasurableSet x) : μ (⋃₀ ↑I) = ∑ c ∈ I.nepowerset with Odd c.card, μ (⋂₀ ↑c) - ∑ c ∈ I.nepowerset with Even c.card, μ (⋂₀ ↑c)