Theorems · Theorem · measure theory

MeasureTheory.Measure.exists_positive_of_not_mutuallySingular

∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  ¬μ.MutuallySingular ν →
    ∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ μ (A ∩ E)

If two finite measures μ and ν are not mutually singular, there exists some ε > 0 and a measurable set E, such that ν(E) > 0 and E is positive with respect to μ - εν. This lemma is useful for the Lebesgue decomposition theorem.

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Cited by

1 results in Mathlib

Foundations

Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure