Measures on Bool

Lemmas about measures on Bool and integrals over Bool.

theorem Bool.cases_set_bool (s : Set Bool) : s = ∅ ∨ s = {true} ∨ s = {false} ∨ s = {true, false}

theorem MeasureTheory.Measure.measure_bool_ext {π₁ π₂ : Measure Bool} (h_false : π₁ {false} = π₂ {false}) (h_true : π₁ {true} = π₂ {true}) : π₁ = π₂

theorem MeasureTheory.Measure.measure_bool_ext_iff {π₁ π₂ : Measure Bool} : π₁ = π₂ ↔ π₁ {false} = π₂ {false} ∧ π₁ {true} = π₂ {true}

theorem Bool.lintegral_bool {f : Bool → ENNReal} (π : MeasureTheory.Measure Bool) : ∫⁻ (x : Bool), f x ∂π = f false * π {false} + f true * π {true}

noncomputable def Bool.boolMeasure (a b : ENNReal) : MeasureTheory.Measure Bool

A measure on Bool constructed from the two values it takes on false and true.

Equations

• Bool.boolMeasure a b = a • MeasureTheory.Measure.dirac false + b • MeasureTheory.Measure.dirac true

@[simp]

theorem Bool.boolMeasure_apply_false (a b : ENNReal) : (boolMeasure a b) {false} = a

@[simp]

theorem Bool.boolMeasure_apply_true (a b : ENNReal) : (boolMeasure a b) {true} = b

@[simp]

theorem Bool.boolMeasure_apply_univ (a b : ENNReal) : (boolMeasure a b) {false, true} = a + b

theorem Bool.measure_eq_boolMeasure (π : MeasureTheory.Measure Bool) : π = boolMeasure (π {false}) (π {true})

theorem Bool.boolMeasure_withDensity (π : MeasureTheory.Measure Bool) (f : Bool → ENNReal) : π.withDensity f = boolMeasure (f false * π {false}) (f true * π {true})

instance Bool.instIsFiniteMeasureBoolMeasureOfReal {x y : ℝ} : MeasureTheory.IsFiniteMeasure (boolMeasure (ENNReal.ofReal x) (ENNReal.ofReal y))