Theorems · Theorem · measure theory

VitaliFamily.exists_measurable_supersets_limRatio

∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ],
  ρ.AbsolutelyContinuous μ →
    ∀ {p q : NNReal},
      p < q →
        ∃ a b,
          MeasurableSet a ∧
            MeasurableSet b ∧ {x | v.limRatio ρ x < ↑p} ⊆ a ∧ {x | ↑q < v.limRatio ρ x} ⊆ b ∧ μ (a ∩ b) = 0

Given two thresholds p < q, the sets {x | v.limRatio ρ x < p} and {x | q < v.limRatio ρ x} are obviously disjoint. The key to proving that v.limRatio ρ is almost everywhere measurable is to show that these sets have measurable supersets which are also disjoint, up to zero measure. This is the content of this lemma.

Defined in

Mathlib.MeasureTheory.Covering.Differentiation

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceSecondCountableTopologyBorelSpaceMeasureTheory.IsLocallyFiniteMeasureMeasureTheory.IsLocallyFiniteMeasure