Theorems · Theorem · measure theory

IsUnifLocDoublingMeasure.ae_tendsto_average_norm_sub

∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {E : Type u_2} [inst_6 : NormedAddCommGroup E] {f : α → E},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ (K : ℝ),
      ∀ᵐ (x : α) ∂μ,
        ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
          Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) →
            (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) →
              Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (nhds 0)

A version of Lebesgue differentiation theorem for a sequence of closed balls whose centers are not required to be fixed.

Defined in

Mathlib.MeasureTheory.Covering.DensityTheorem

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceMeasurableSpaceIsUnifLocDoublingMeasureSecondCountableTopologyBorelSpaceMeasureTheory.IsLocallyFiniteMeasureNormedAddCommGroup