class FinitelyAdditiveMeasure {X : Type u_1} (B : ConcreteBooleanAlgebra X) : Type u_1

Definition 1.4.19 (Finitely additive measure)

• measure : Set X → EReal
• measure_pos (A : Set X) : ConcreteBooleanAlgebra.measurable A → 0 ≤ measure B A
• measure_empty : measure B ∅ = 0
• measure_finite_additive (E F : Set X) : ConcreteBooleanAlgebra.measurable E → ConcreteBooleanAlgebra.measurable F → Disjoint E F → measure B (E ∪ F) = measure B E + measure B F

theorem FinitelyAdditiveMeasure.ext {X : Type u_1} {B : ConcreteBooleanAlgebra X} {μ ν : FinitelyAdditiveMeasure B} (h : ∀ (A : Set X), measure B A = measure B A) : μ = ν

Two finitely additive measures on the same algebra are equal as soon as they assign the same value to every set; the other fields are propositions, so proof irrelevance disposes of them. Tagged so that the ext tactic applies to these measures.

theorem FinitelyAdditiveMeasure.ext_iff {X : Type u_1} {B : ConcreteBooleanAlgebra X} {μ ν : FinitelyAdditiveMeasure B} : μ = ν ↔ ∀ (A : Set X), measure B A = measure B A

noncomputable def FinitelyAdditiveMeasure.lebesgue (d : ℕ) : FinitelyAdditiveMeasure (LebesgueMeasurable.boolean_algebra d)

Example 1.4.21 (Lebesgue measure)

Equations

• FinitelyAdditiveMeasure.lebesgue d = { measure := fun (A : Set (EuclideanSpace' d)) => Lebesgue_measure A, measure_pos := ⋯, measure_empty := ⋯, measure_finite_additive := ⋯ }

def FinitelyAdditiveMeasure.restrict_alg {X : Type u_1} {B : ConcreteBooleanAlgebra X} (μ : FinitelyAdditiveMeasure B) {B' : ConcreteBooleanAlgebra X} (hBB' : B' ≤ B) : FinitelyAdditiveMeasure B'

Example 1.4.21 (restriction to a subalgebra)

Equations

• μ.restrict_alg hBB' = { measure := FinitelyAdditiveMeasure.measure B, measure_pos := ⋯, measure_empty := ⋯, measure_finite_additive := ⋯ }

noncomputable def FinitelyAdditiveMeasure.jordan (d : ℕ) : FinitelyAdditiveMeasure (JordanMeasurable.boolean_algebra d)

Example 1.4.21 (Jordan measure)

Equations

• FinitelyAdditiveMeasure.jordan d = (FinitelyAdditiveMeasure.lebesgue d).restrict_alg ⋯

noncomputable def FinitelyAdditiveMeasure.null (d : ℕ) : FinitelyAdditiveMeasure (IsNull.boolean_algebra d)

Example 1.4.21 (null sets)

Equations

• FinitelyAdditiveMeasure.null d = (FinitelyAdditiveMeasure.lebesgue d).restrict_alg ⋯

noncomputable def FinitelyAdditiveMeasure.elem (d : ℕ) : FinitelyAdditiveMeasure (EuclideanSpace'.elementary_boolean_algebra d)

Example 1.4.21 (elementary sets)

Equations

• FinitelyAdditiveMeasure.elem d = (FinitelyAdditiveMeasure.lebesgue d).restrict_alg ⋯

noncomputable def FinitelyAdditiveMeasure.dirac {X : Type u_1} (x₀ : X) (B : ConcreteBooleanAlgebra X) : FinitelyAdditiveMeasure B

Example 1.4.22 (Dirac measure)

Equations

• FinitelyAdditiveMeasure.dirac x₀ B = { measure := fun (A : Set X) => if x₀ ∈ A then 1 else 0, measure_pos := ⋯, measure_empty := ⋯, measure_finite_additive := ⋯ }

@[implicit_reducible]

noncomputable instance FinitelyAdditiveMeasure.instZero {X : Type u_1} (B : ConcreteBooleanAlgebra X) : Zero (FinitelyAdditiveMeasure B)

Example 1.4.23 (Zero measure)

Equations

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

@[implicit_reducible]

noncomputable instance FinitelyAdditiveMeasure.instAdd {X : Type u_1} {B : ConcreteBooleanAlgebra X} : Add (FinitelyAdditiveMeasure B)

Example 1.4.24 (linear combinations of measures)

Equations

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

@[implicit_reducible]

noncomputable instance FinitelyAdditiveMeasure.instSmul {X : Type u_1} {B : ConcreteBooleanAlgebra X} : SMul ENNReal (FinitelyAdditiveMeasure B)

Equations

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

@[implicit_reducible]

noncomputable instance FinitelyAdditiveMeasure.instAddCommMonoid {X : Type u_1} {B : ConcreteBooleanAlgebra X} : AddCommMonoid (FinitelyAdditiveMeasure B)

Equations

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

@[implicit_reducible]

noncomputable instance FinitelyAdditiveMeasure.instDistribMulAction {X : Type u_1} {B : ConcreteBooleanAlgebra X} : DistribMulAction ENNReal (FinitelyAdditiveMeasure B)

Equations

• FinitelyAdditiveMeasure.instDistribMulAction = { toSMul := FinitelyAdditiveMeasure.instSmul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

def FinitelyAdditiveMeasure.restrict {X : Type u_1} {B : ConcreteBooleanAlgebra X} (μ : FinitelyAdditiveMeasure B) (A : Set X) (hA : ConcreteBooleanAlgebra.measurable A) : FinitelyAdditiveMeasure (B.restrict A)

Example 1.4.25 (Restriction of a measure)

Equations

• μ.restrict A hA = { measure := fun (E : Set ↑A) => FinitelyAdditiveMeasure.measure B (Subtype.val '' E), measure_pos := ⋯, measure_empty := ⋯, measure_finite_additive := ⋯ }

noncomputable def FinitelyAdditiveMeasure.counting (X : Type u_1) : FinitelyAdditiveMeasure ⊤

Example 1.4.26 (Counting a measure)

Equations

• FinitelyAdditiveMeasure.counting X = { measure := fun (E : Set X) => ↑↑(ENat.card ↑E), measure_pos := ⋯, measure_empty := ⋯, measure_finite_additive := ⋯ }

theorem ConcreteBooleanAlgebra.inter_mem {X : Type u_1} (B : ConcreteBooleanAlgebra X) {E F : Set X} (hE : measurable E) (hF : measurable F) : measurable (E ∩ F)

Boolean algebras are closed under intersection.

theorem ConcreteBooleanAlgebra.diff_mem {X : Type u_1} (B : ConcreteBooleanAlgebra X) {E F : Set X} (hE : measurable E) (hF : measurable F) : measurable (E \ F)

Boolean algebras are closed under set difference.

theorem ConcreteBooleanAlgebra.finite_biUnion_mem {X : Type u_1} {J : Type u_2} (B : ConcreteBooleanAlgebra X) {I : Finset J} {E : J → Set X} (hE : ∀ (j : J), measurable (E j)) : measurable (⋃ j ∈ I, E j)

Boolean algebras are closed under finite unions.

theorem FinitelyAdditiveMeasure.mono {X : Type u_1} {B : ConcreteBooleanAlgebra X} (μ : FinitelyAdditiveMeasure B) {E F : Set X} (hE : ConcreteBooleanAlgebra.measurable E) (hF : ConcreteBooleanAlgebra.measurable F) (hsub : E ⊆ F) : measure B E ≤ measure B F

Exercise 1.4.20(i)

theorem FinitelyAdditiveMeasure.finite_additivity {X : Type u_1} {B : ConcreteBooleanAlgebra X} (μ : FinitelyAdditiveMeasure B) {J : Type u_2} {I : Finset J} {E : J → Set X} (hE : ∀ (j : J), ConcreteBooleanAlgebra.measurable (E j)) (hdisj : Set.univ.PairwiseDisjoint E) : measure B (⋃ j ∈ I, E j) = ∑ j ∈ I, measure B (E j)

Exercise 1.4.20(ii)

theorem FinitelyAdditiveMeasure.finite_subadditivity {X : Type u_1} {B : ConcreteBooleanAlgebra X} (μ : FinitelyAdditiveMeasure B) {J : Type u_2} {I : Finset J} {E : J → Set X} (hE : ∀ (j : J), ConcreteBooleanAlgebra.measurable (E j)) : measure B (⋃ j ∈ I, E j) ≤ ∑ j ∈ I, measure B (E j)

Exercise 1.4.20(iii)

theorem FinitelyAdditiveMeasure.mes_union_add_mes_inter {X : Type u_1} {B : ConcreteBooleanAlgebra X} (μ : FinitelyAdditiveMeasure B) {E F : Set X} (hE : ConcreteBooleanAlgebra.measurable E) (hF : ConcreteBooleanAlgebra.measurable F) : measure B (E ∪ F) + measure B (E ∩ F) = measure B E + measure B F

Exercise 1.4.20(iv)

theorem FinitelyAdditiveMeasure.finite_atomic_eq {I : Type u_1} {X : Type u_2} [Fintype I] {atoms : I → Set X} (h_part : IsPartition atoms) (μ : FinitelyAdditiveMeasure h_part.to_ConcreteBooleanAlgebra) : ∃! c : I → ENNReal, ∀ (E : Set X), ConcreteBooleanAlgebra.measurable E → measure h_part.to_ConcreteBooleanAlgebra E = ↑(∑ i : I with atoms i ⊆ E, c i)

Exercise 1.4.21

class CountablyAdditiveMeasure {X : Type u_1} (B : ConcreteSigmaAlgebra X) extends FinitelyAdditiveMeasure B.toConcreteBooleanAlgebra : Type u_1

Definition 1.4.27 (Countably additive measure)

• measure : Set X → EReal
• measure_pos (A : Set X) : ConcreteBooleanAlgebra.measurable A → 0 ≤ measure B.toConcreteBooleanAlgebra A
• measure_empty : measure B.toConcreteBooleanAlgebra ∅ = 0
• measure_finite_additive (E F : Set X) : ConcreteBooleanAlgebra.measurable E → ConcreteBooleanAlgebra.measurable F → Disjoint E F → measure B.toConcreteBooleanAlgebra (E ∪ F) = measure B.toConcreteBooleanAlgebra E + measure B.toConcreteBooleanAlgebra F
• measure_countable_additive (E : ℕ → Set X) : (∀ (n : ℕ), ConcreteBooleanAlgebra.measurable (E n)) → Set.univ.PairwiseDisjoint E → FinitelyAdditiveMeasure.measure B.toConcreteBooleanAlgebra (⋃ (n : ℕ), E n) = ∑' (n : ℕ), FinitelyAdditiveMeasure.measure B.toConcreteBooleanAlgebra (E n)

theorem CountablyAdditiveMeasure.ext {X : Type u_1} {B : ConcreteSigmaAlgebra X} {μ ν : CountablyAdditiveMeasure B} (h : ∀ (A : Set X), FinitelyAdditiveMeasure.measure B.toConcreteBooleanAlgebra A = FinitelyAdditiveMeasure.measure B.toConcreteBooleanAlgebra A) : μ = ν

The analogue of FinitelyAdditiveMeasure.ext for countably additive measures. The underlying finitely additive measure is an instance-implicit parent field, so it is enough to know the two agree on every set.

theorem CountablyAdditiveMeasure.ext_iff {X : Type u_1} {B : ConcreteSigmaAlgebra X} {μ ν : CountablyAdditiveMeasure B} : μ = ν ↔ ∀ (A : Set X), FinitelyAdditiveMeasure.measure B.toConcreteBooleanAlgebra A = FinitelyAdditiveMeasure.measure B.toConcreteBooleanAlgebra A

def FinitelyAdditiveMeasure.isCountablyAdditive {X : Type u_1} {B : ConcreteBooleanAlgebra X} (μ : FinitelyAdditiveMeasure B) : Prop

Equations

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

def FinitelyAdditiveMeasure.isCountablyAdditive.toCountablyAdditive {X : Type u_1} {B : ConcreteBooleanAlgebra X} (μ : FinitelyAdditiveMeasure B) (h : μ.isCountablyAdditive) : CountablyAdditiveMeasure ⋯.toSigmaAlgebra

Equations

• FinitelyAdditiveMeasure.isCountablyAdditive.toCountablyAdditive μ h = { toFinitelyAdditiveMeasure := μ, measure_countable_additive := ⋯ }

theorem FinitelyAdditiveMeasure.lebesgue_isCountablyAdditive (d : ℕ) : (lebesgue d).isCountablyAdditive

Example 1.4.28

theorem FinitelyAdditiveMeasure.isCountablyAdditive_restrict_alg {X : Type u_1} {B B' : ConcreteSigmaAlgebra X} (μ : CountablyAdditiveMeasure B) (hBB' : B' ≤ B) : (μ.restrict_alg hBB').isCountablyAdditive

def CountablyAdditiveMeasure.restrict_alg {X : Type u_1} {B B' : ConcreteSigmaAlgebra X} (μ : CountablyAdditiveMeasure B) (hBB' : B' ≤ B) : CountablyAdditiveMeasure B'

Equations

• μ.restrict_alg hBB' = { toFinitelyAdditiveMeasure := μ.restrict_alg hBB', measure_countable_additive := ⋯ }

theorem FinitelyAdditiveMeasure.dirac_isCountablyAdditive {X : Type u_1} (x₀ : X) (B : ConcreteBooleanAlgebra X) (hB : B.isSigmaAlgebra) : (dirac x₀ B).isCountablyAdditive

Example 1.4.29 (Dirac measure)

theorem FinitelyAdditiveMeasure.counting_isCountablyAdditive {X : Type u_1} : (counting X).isCountablyAdditive

Example 1.4.29 (Counting measure)

def CountablyAdditiveMeasure.restrict {X : Type u_1} {B : ConcreteSigmaAlgebra X} (μ : CountablyAdditiveMeasure B) (A : Set X) (hA : ConcreteBooleanAlgebra.measurable A) : CountablyAdditiveMeasure (B.restrict A)

Example 1.4.30

Equations

• μ.restrict A hA = { toFinitelyAdditiveMeasure := μ.restrict A hA, measure_countable_additive := ⋯ }

@[implicit_reducible]

noncomputable instance CountablyAdditiveMeasure.instZero {X : Type u_1} (B : ConcreteSigmaAlgebra X) : Zero (CountablyAdditiveMeasure B)

Equations

• CountablyAdditiveMeasure.instZero B = { zero := let __FinitelyAdditiveMeasure := 0; { toFinitelyAdditiveMeasure := __FinitelyAdditiveMeasure, measure_countable_additive := ⋯ } }

@[implicit_reducible]

noncomputable instance CountablyAdditiveMeasure.instAdd {X : Type u_1} {B : ConcreteSigmaAlgebra X} : Add (CountablyAdditiveMeasure B)

Equations

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

@[implicit_reducible]

noncomputable instance CountablyAdditiveMeasure.instAddCommMonoid {X : Type u_1} {B : ConcreteSigmaAlgebra X} : AddCommMonoid (CountablyAdditiveMeasure B)

Equations

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

@[implicit_reducible]

noncomputable instance CountablyAdditiveMeasure.instSmul {X : Type u_1} {B : ConcreteSigmaAlgebra X} : SMul ENNReal (CountablyAdditiveMeasure B)

Exercise 1.4.22(i)

Equations

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

@[implicit_reducible]

noncomputable instance CountablyAdditiveMeasure.instDistribMulAction {X : Type u_1} {B : ConcreteSigmaAlgebra X} : DistribMulAction ENNReal (CountablyAdditiveMeasure B)

Equations

• CountablyAdditiveMeasure.instDistribMulAction = { toSMul := CountablyAdditiveMeasure.instSmul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

noncomputable def CountablyAdditiveMeasure.sum {X : Type u_1} {B : ConcreteSigmaAlgebra X} (μ : ℕ → CountablyAdditiveMeasure B) : CountablyAdditiveMeasure B

Exercise 1.4.22(ii)

Equations

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

noncomputable def CountablyAdditiveMeasure.toMeasure {X : Type u_1} {B : ConcreteSigmaAlgebra X} (μ : CountablyAdditiveMeasure B) : MeasureTheory.Measure X

Equations

• μ.toMeasure = { measureOf := fun (E : Set X) => (FinitelyAdditiveMeasure.measure B.toConcreteBooleanAlgebra E).toENNReal, empty := ⋯, mono := ⋯, iUnion_nat := ⋯, m_iUnion := ⋯, trim_le := ⋯ }

noncomputable def FinitelyAdditiveMeasure.isCountablyAdditive.toMeasure {X : Type u_1} {B : ConcreteBooleanAlgebra X} {μ : FinitelyAdditiveMeasure B} (h : μ.isCountablyAdditive) : MeasureTheory.Measure X

Equations

• h.toMeasure = (FinitelyAdditiveMeasure.isCountablyAdditive.toCountablyAdditive μ h).toMeasure

def Measure.toCountablyAdditiveMeasure {X : Type u_1} [M : MeasurableSpace X] (μ : MeasureTheory.Measure X) : CountablyAdditiveMeasure M.sigmaAlgebra

Equations

• Measure.toCountablyAdditiveMeasure μ = { measure := fun (E : Set X) => ↑(μ.measureOf E), measure_pos := ⋯, measure_empty := ⋯, measure_finite_additive := ⋯, measure_countable_additive := ⋯ }

theorem Measure.countable_subadditivity {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {E : ℕ → Set X} (hE : ∀ (n : ℕ), Measurable (E n)) : μ.measureOf (⋃ (n : ℕ), E n) ≤ ∑' (n : ℕ), μ.measureOf (E n)

Exercise 1.4.23(i)

theorem Measure.upwards_mono {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {E : ℕ → Set X} (hE : ∀ (n : ℕ), Measurable (E n)) (hmono : Monotone E) : μ (⋃ (n : ℕ), E n) = ⨆ (n : ℕ), μ.measureOf (E n)

Exercise 1.4.23(ii)

theorem Measure.downwards_mono {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {E : ℕ → Set X} (hE : ∀ (n : ℕ), Measurable (E n)) (hmono : Antitone E) (hfin : ∃ (n : ℕ), μ (E n) < ⊤) : μ (⋂ (n : ℕ), E n) = ⨅ (n : ℕ), μ.measureOf (E n)

Exercise 1.4.23(iii)

theorem Measure.downwards_mono_counter : ∃ (X : Type) (M : MeasurableSpace X) (μ : MeasureTheory.Measure X) (E : ℕ → Set X) (_ : ∀ (n : ℕ), Measurable (E n)) (_ : Antitone E), μ (⋂ (n : ℕ), E n) ≠ ⨅ (n : ℕ), μ.measureOf (E n)

theorem Measure.measurable_of_lim {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {E : ℕ → Set X} (hE : ∀ (n : ℕ), Measurable (E n)) {E' : Set X} (hlim : PointwiseConvergesTo E E') : Measurable E'

Exercise 1.4.24 (i) (Dominated convergence for sets)

theorem Measure.measure_of_lim {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {E : ℕ → Set X} (hE : ∀ (n : ℕ), Measurable (E n)) {E' F : Set X} (hlim : PointwiseConvergesTo E E') (hF : Measurable F) (hfin : μ F < ⊤) (hcon : ∀ (n : ℕ), E n ⊆ F) : Filter.Tendsto (fun (n : ℕ) => μ (E n)) Filter.atTop (nhds (μ E'))

Exercise 1.4.24 (ii) (Dominated convergence for sets)

theorem Measure.measure_of_lim_counter : ∃ (X : Type) (M : MeasurableSpace X) (μ : MeasureTheory.Measure X) (E : ℕ → Set X) (_ : ∀ (n : ℕ), Measurable (E n)) (E' : Set X) (F : Set X) (_ : PointwiseConvergesTo E E') (_ : Measurable F) (_ : ∀ (n : ℕ), E n ⊆ F), ¬Filter.Tendsto (fun (n : ℕ) => μ (E n)) Filter.atTop (nhds (μ E'))

Exercise 1.4.24 (iii) (Dominated convergence for sets)

theorem Measure.on_countable {X : Type u_1} [Countable X] [M : MeasurableSpace X] (hM : M = ⊤) (μ : MeasureTheory.Measure X) : ∃! c : X → ENNReal, ∀ (E : Set X), μ E = ∑' (x : ↑E), c ↑x

Exercise 1.4.25

theorem Measure.completion_lt {X : Type u_1} [M : MeasurableSpace X] (μ : MeasureTheory.Measure X) (M' : MeasurableSpace X) (μ' : MeasureTheory.Measure X) (hcomplete : μ'.IsComplete) (hMM' : M ≤ M') (hμ : ∀ (E : Set X), MeasurableSpace.MeasurableSet' M E → μ E = μ' E) (E : Set X) : MeasureTheory.NullMeasurableSet E μ → MeasurableSpace.MeasurableSet' M' E ∧ μ' E = μ.completion E

Exercise 1.4.26 (Completion)

noncomputable def EuclideanSpace'.lebesgueMeasure (d : ℕ) : MeasureTheory.Measure (EuclideanSpace' d)

Equations

• EuclideanSpace'.lebesgueMeasure d = ⋯.toMeasure

noncomputable def EuclideanSpace'.borelMeasure (d : ℕ) : MeasureTheory.Measure (EuclideanSpace' d)

Equations

• EuclideanSpace'.borelMeasure d = ((FinitelyAdditiveMeasure.isCountablyAdditive.toCountablyAdditive (FinitelyAdditiveMeasure.lebesgue d) ⋯).restrict_alg ⋯).toMeasure

def Measure.equiv {X : Type u_1} {M M' : MeasurableSpace X} (μ : MeasureTheory.Measure X) (μ' : MeasureTheory.Measure X) : Prop

Equations

• Measure.equiv μ μ' = (M = M' ∧ ∀ (E : Set X), MeasurableSpace.MeasurableSet' M E → μ E = μ' E)

theorem EuclideanSpace'.borel_completion_eq_lebesgue {d : ℕ} : Measure.equiv (borelMeasure d).completion (lebesgueMeasure d)

Exercise 1.4.27

theorem BooleanAlgebra.approx_finite {X : Type u_1} {B : ConcreteBooleanAlgebra X} (μ : MeasureTheory.Measure X) (hfin : μ Set.univ < ⊤) (ε : ℝ) (hε : ε > 0) (E : Set X) (hE : ConcreteBooleanAlgebra.measurable E) : ∃ (F : Set X), ConcreteBooleanAlgebra.measurable F ∧ μ (symmDiff E F) < ENNReal.ofReal ε

Exercise 1.4.28(i) (Approximation by an algebra)

theorem BooleanAlgebra.approx_sigma_finite {X : Type u_1} {B : ConcreteBooleanAlgebra X} (μ : MeasureTheory.Measure X) (hσfin : ∃ (A : ℕ → Set X), (∀ (n : ℕ), ConcreteBooleanAlgebra.measurable (A n) ∧ μ (A n) < ⊤) ∧ ⋃ (n : ℕ), A n = ⊤) (ε : ℝ) (hε : ε > 0) (E : Set X) (hE : ConcreteBooleanAlgebra.measurable E) (hEfin : μ E < ⊤) : ∃ (F : Set X), ConcreteBooleanAlgebra.measurable F ∧ μ (symmDiff E F) < ENNReal.ofReal ε

Exercise 1.4.28(ii) (Approximation by an algebra)