Zero-one measures

We introduce the typeclass IsZeroOneMeasure for measures that only take the values 0 and 1.

class MeasureTheory.IsZeroOneMeasure {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) : Prop

A measure is a zero-one measure if it only takes the values 0 or 1.

• zero_one₀ ⦃s : Set α⦄ : MeasurableSet s → μ s = 0 ∨ μ s = 1

theorem MeasureTheory.Measure.zero_one {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) [IsZeroOneMeasure μ] (s : Set α) : μ s = 0 ∨ μ s = 1

instance MeasureTheory.instIsZeroOrProbabilityMeasure {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [IsZeroOneMeasure μ] : IsZeroOrProbabilityMeasure μ

theorem MeasureTheory.IsZeroOneMeasure.exists_measure_eq_one_iff_measure_univ_eq_one {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [IsZeroOneMeasure μ] : (∃ (s : Set α), μ s = 1) ↔ μ Set.univ = 1

theorem MeasureTheory.IsZeroOneMeasure.measure_univ {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [IsZeroOneMeasure μ] {s : Set α} (hμs : μ s = 1) : μ Set.univ = 1

theorem MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [IsZeroOneMeasure μ] {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s = 1) (hμt : μ t = 1) : μ (s ∩ t) = 1

theorem MeasureTheory.IsZeroOneMeasure.measure_inter_eq_prod {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [IsZeroOneMeasure μ] {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) : μ (s ∩ t) = μ s * μ t