Lebesgue points along concentric closed balls

Mathlib's IsUnifLocDoublingMeasure.ae_tendsto_average_norm_sub states the Lebesgue differentiation theorem for a uniformly locally doubling measure along arbitrary families of closed balls shrinking to a point. This file records its most common special case: almost every point x is a Lebesgue point of a locally integrable function f in the sense that the mean oscillation ⨍_{closedBall x r} ‖f - f x‖ tends to zero as r → 0⁺, and the analogous statement for the averages of an integrable ℝ≥0∞-valued function. For an additive Haar measure on a finite-dimensional real normed space, spheres are null, so the same averages over open balls converge as well.

theorem IsUnifLocDoublingMeasure.ae_tendsto_average_closedBall_norm_sub {α : Type u_1} {E : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] [NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.LocallyIntegrable f μ) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (r : ℝ) => ⨍ (y : α) in Metric.closedBall x r, ‖f y - f x‖ ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Lebesgue differentiation theorem along concentric closed balls. For a uniformly locally doubling measure, almost every point x is a Lebesgue point of a locally integrable function f: the mean oscillation ⨍_{closedBall x r} ‖f - f x‖ tends to zero as r → 0⁺.

theorem IsUnifLocDoublingMeasure.ae_tendsto_setLAverage_closedBall {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → ENNReal} (hf : AEMeasurable f μ) (hfin : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (r : ℝ) => ⨍⁻ (y : α) in Metric.closedBall x r, f y ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

Lebesgue differentiation theorem along concentric closed balls, for ℝ≥0∞-valued functions. For a uniformly locally doubling measure and an a.e. measurable f with finite integral, the averages ⨍_{closedBall x r} f tend to f x as r → 0⁺ for almost every x.

theorem MeasureTheory.Measure.ae_tendsto_setLAverage_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] {f : E → ENNReal} (hf : AEMeasurable f μ) (hfin : ∫⁻ (x : E), f x ∂μ ≠ ⊤) : ∀ᵐ (x : E) ∂μ, Filter.Tendsto (fun (r : ℝ) => ⨍⁻ (y : E) in Metric.ball x r, f y ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

Lebesgue differentiation theorem along concentric open balls, for an additive Haar measure. For an a.e. measurable f : E → ℝ≥0∞ with finite integral, the averages ⨍_{ball x r} f tend to f x as r → 0⁺ for almost every x. Open and closed balls of positive radius differ by a null set, so this is IsUnifLocDoublingMeasure.ae_tendsto_setLAverage_closedBall for open balls.