structure MeasureTheory.MonotoneClass (α : Type u_2) : Type u_2

A monotone class is a collection of subsets of a type α that is closed under countable monotone union and countable antitone intersection.

• Has : Set α → Prop

  Predicate saying that a given set is contained in the Monotone Class.

• has_iUnion {A : ℕ → Set α} : (∀ (n : ℕ), self.Has (A n)) → Monotone A → self.Has (⋃ (n : ℕ), A n)

  A monotone class is closed under countable monotone union.

• has_iInter (B : ℕ → Set α) : (∀ (n : ℕ), self.Has (B n)) → Antitone B → self.Has (⋂ (n : ℕ), B n)

  A monotone class is closed under countable antitone intersection.

theorem MeasureTheory.MonotoneClass.ext {α : Type u_1} {C₁ C₂ : MonotoneClass α} : (∀ (s : Set α), C₁.Has s ↔ C₂.Has s) → C₁ = C₂

theorem MeasureTheory.MonotoneClass.ext_iff {α : Type u_1} {C₁ C₂ : MonotoneClass α} : C₁ = C₂ ↔ ∀ (s : Set α), C₁.Has s ↔ C₂.Has s

theorem MeasureTheory.MonotoneClass.has_iUnion' {α : Type u_1} (C : MonotoneClass α) {β : Type u_2} [Nonempty β] [Countable β] [LinearOrder β] {A : β → Set α} (hC : ∀ (i : β), C.Has (A i)) (h_mono : Monotone A) : C.Has (⋃ (i : β), A i)

theorem MeasureTheory.MonotoneClass.has_iInter' {α : Type u_1} (C : MonotoneClass α) {β : Type u_2} [Nonempty β] [Countable β] [LinearOrder β] {A : β → Set α} (hC : ∀ (i : β), C.Has (A i)) (h_mono : Antitone A) : C.Has (⋂ (i : β), A i)

instance MeasureTheory.MonotoneClass.instLEMonotoneClass {α : Type u_1} : LE (MonotoneClass α)

Equations

• MeasureTheory.MonotoneClass.instLEMonotoneClass = { le := fun (C₁ C₂ : MeasureTheory.MonotoneClass α) => C₁.Has ≤ C₂.Has }

theorem MeasureTheory.MonotoneClass.le_def {α : Type u_1} {C₁ C₂ : MonotoneClass α} : C₁ ≤ C₂ ↔ C₁.Has ≤ C₂.Has

instance MeasureTheory.MonotoneClass.instPartialOrder {α : Type u_1} : PartialOrder (MonotoneClass α)

Equations

• One or more equations did not get rendered due to their size.

theorem MeasurableSpace.DynkinSystem.has_iUnion_of_mono {α : Type u_3} (d : DynkinSystem α) {A : ℕ → Set α} (h_mono : Monotone A) (hA : ∀ (i : ℕ), d.Has (A i)) : d.Has (⋃ (i : ℕ), A i)

theorem MeasurableSpace.DynkinSystem.has_iInter_of_anti {α : Type u_3} (d : DynkinSystem α) {B : ℕ → Set α} (h_anti : Antitone B) (hB : ∀ (i : ℕ), d.Has (B i)) : d.Has (⋂ (i : ℕ), B i)

def MeasureTheory.MonotoneClass.ofDynkinSystem {α : Type u_1} (d : MeasurableSpace.DynkinSystem α) : MonotoneClass α

Every Dynkin system forms a Monotone class.

Equations

• MeasureTheory.MonotoneClass.ofDynkinSystem d = { Has := d.Has, has_iUnion := ⋯, has_iInter := ⋯ }

theorem MeasureTheory.MonotoneClass.ofDynkinSystem_le_ofDynkinSystem_iff {α : Type u_1} {d₁ d₂ : MeasurableSpace.DynkinSystem α} : ofDynkinSystem d₁ ≤ ofDynkinSystem d₂ ↔ d₁ ≤ d₂

def MeasureTheory.MonotoneClass.ofMeasurableSpace {α : Type u_1} (m : MeasurableSpace α) : MonotoneClass α

Every σ-algebra forms a Monotone class.

Equations

• MeasureTheory.MonotoneClass.ofMeasurableSpace m = MeasureTheory.MonotoneClass.ofDynkinSystem (MeasurableSpace.DynkinSystem.ofMeasurableSpace m)

theorem MeasureTheory.MonotoneClass.ofMeasurableSpace_le_ofMeasurableSpace_iff {α : Type u_1} {m₁ m₂ : MeasurableSpace α} : ofMeasurableSpace m₁ ≤ ofMeasurableSpace m₂ ↔ m₁ ≤ m₂

inductive MeasureTheory.MonotoneClass.GenerateHas {α : Type u_1} (s : Set (Set α)) : Set α → Prop

The least MonotoneClass containing a collection of basic sets. This inductive type gives the underlying collection of sets.

• basic {α : Type u_1} {s : Set (Set α)} (t : Set α) : t ∈ s → GenerateHas s t
• iUnion {α : Type u_1} {s : Set (Set α)} {A : ℕ → Set α} : (∀ (n : ℕ), GenerateHas s (A n)) → Monotone A → GenerateHas s (⋃ (n : ℕ), A n)
• iInter {α : Type u_1} {s : Set (Set α)} {B : ℕ → Set α} : (∀ (n : ℕ), GenerateHas s (B n)) → Antitone B → GenerateHas s (⋂ (n : ℕ), B n)

def MeasureTheory.MonotoneClass.generate {α : Type u_1} (s : Set (Set α)) : MonotoneClass α

The least MonotoneClass containing a collection of basic sets.

Equations

• MeasureTheory.MonotoneClass.generate s = { Has := MeasureTheory.MonotoneClass.GenerateHas s, has_iUnion := ⋯, has_iInter := ⋯ }

theorem MeasureTheory.MonotoneClass.generateHas_def {α : Type u_1} {s : Set (Set α)} : (generate s).Has = GenerateHas s

theorem MeasureTheory.MonotoneClass.generateHas_compl {α : Type u_1} {s : Set (Set α)} (hs : IsSetAlgebra s) {t : Set α} (ht : (generate s).Has t) : (generate s).Has tᶜ

theorem MeasureTheory.MonotoneClass.generateHas_inter {α : Type u_1} {s : Set (Set α)} (hs : IsSetAlgebra s) {t u : Set α} (ht : (generate s).Has t) (hu : (generate s).Has u) : (generate s).Has (t ∩ u)

If s is an algebra of sets, then the monotone class generated by s is closed under intersections.

theorem MeasureTheory.MonotoneClass.isSetAlgebra_generateHas {α : Type u_1} {s : Set (Set α)} (hs : IsSetAlgebra s) : IsSetAlgebra (generate s).Has

If s is an algebra of sets, then the monotone class it generates is an algebra of sets.

theorem MeasureTheory.MonotoneClass.generate_le {α : Type u_1} (C : MonotoneClass α) {s : Set (Set α)} (h : ∀ t ∈ s, C.Has t) : generate s ≤ C

The monotone class generated by s is the smallest monotone class containing s.

theorem MeasureTheory.MonotoneClass.generate_has_subset_generate_measurable {α : Type u_1} {s : Set (Set α)} {S : Set α} (hS : (generate s).Has S) : MeasurableSet S

If a set belongs to the monotone class generated by s, then it is measurable for the σ-algebra generated by s.

instance MeasureTheory.MonotoneClass.instInhabited {α : Type u_1} : Inhabited (MonotoneClass α)

Equations

• MeasureTheory.MonotoneClass.instInhabited = { default := MeasureTheory.MonotoneClass.generate Set.univ }

def MeasureTheory.MonotoneClass.toMeasurableSpace {α : Type u_1} (C : MonotoneClass α) (h : IsSetAlgebra C.Has) : MeasurableSpace α

If a Monotone class is a set algebra, then it forms a σ-algebra.

Equations

• C.toMeasurableSpace h = { MeasurableSet' := C.Has, measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }

theorem MeasureTheory.MonotoneClass.ofMeasurableSpace_toMeasurableSpace {α : Type u_1} (C : MonotoneClass α) (h : IsSetAlgebra C.Has) : ofMeasurableSpace (C.toMeasurableSpace h) = C

theorem MeasureTheory.MonotoneClass.generateFrom_eq {α : Type u_1} {s : Set (Set α)} (hs : IsSetAlgebra s) : MeasurableSpace.MeasurableSet' (MeasurableSpace.generateFrom s) = (generate s).Has

Monotone Class theorem:

Given a set algebra s. Then the monotone class generated by s is equal to the σ-algebra generated by s.

theorem MeasureTheory.induction_on_monotone {α : Type u_1} {m : MeasurableSpace α} {C : (s : Set α) → MeasurableSet s → Prop} {s : Set (Set α)} (h_eq : m = MeasurableSpace.generateFrom s) (h_inter : IsSetAlgebra s) (basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯) (iUnion : ∀ (A : ℕ → Set α), Monotone A → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (A i)), (∀ (i : ℕ), C (A i) ⋯) → C (⋃ (i : ℕ), A i) ⋯) (iInter : ∀ (A : ℕ → Set α), Antitone A → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (A i)), (∀ (i : ℕ), C (A i) ⋯) → C (⋂ (i : ℕ), A i) ⋯) (t : Set α) (ht : MeasurableSet t) : C t ht

Induction principle for measurable sets based on the Monotone Class theorem. If s is a set algebra that generates the σ-algebra on α and a predicate C defined on measurable sets is true

• on each set t ∈ s;
• on the union of monotone sequences of measurable sets that satisfy C;
• on the intersection of antitone sequences of measurable sets that satisfy C,

then it is true on all measurable sets in α.