Theorems · Theorem · measure theory

VitaliFamily.measure_le_of_frequently_le

∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] {ρ : MeasureTheory.Measure α}
  (ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure ν],
  ρ.AbsolutelyContinuous μ → ∀ (s : Set α), (∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a) → ρ s ≤ ν s

If two measures ρ and ν have, at every point of a set s, arbitrarily small sets in a Vitali family satisfying ρ a ≤ ν a, then ρ s ≤ ν s if ρ ≪ μ.

Defined in

Mathlib.MeasureTheory.Covering.Differentiation

Cited by

5 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceSecondCountableTopologyBorelSpaceMeasureTheory.IsLocallyFiniteMeasure