Lebesgue differentiation on the line for extended nonnegative densities

Mathlib's IntervalIntegrable.ae_hasDerivAt_integral differentiates the primitive of an interval-integrable Bochner integrand. This file records the companion statement for an extended nonnegative density and the lower Lebesgue integral: if f : ℝ → ℝ≥0∞ is almost everywhere measurable on Ι a b with finite lower integral there, then at almost every point t of [a, b] the averages (∫⁻ r in Ι t s, f r) / edist s t tend to f t as s → t with s ≠ t, from either side.

Stating it for ℝ≥0∞-valued densities avoids choosing a real representative of f and the ENNReal.toReal bookkeeping that comes with it, which is the convenient form when the density bounds a distance from above, as for the metric derivative of a curve.

Main results

• TauCeti.ae_tendsto_setLIntegral_uIoc_div: the one-dimensional Lebesgue differentiation theorem for an extended nonnegative density which is almost everywhere measurable with finite lower integral on an interval.

theorem TauCeti.ae_tendsto_setLIntegral_uIoc_div {f : ℝ → ENNReal} {a b : ℝ} (hf : AEMeasurable f (MeasureTheory.volume.restrict (Set.uIoc a b))) (hfin : ∫⁻ (r : ℝ) in Set.uIoc a b, f r ≠ ⊤) : ∀ᵐ (t : ℝ), t ∈ Set.uIcc a b → Filter.Tendsto (fun (s : ℝ) => (∫⁻ (r : ℝ) in Set.uIoc t s, f r) / edist s t) (nhdsWithin t {t}ᶜ) (nhds (f t))

The Lebesgue differentiation theorem on the line for an extended nonnegative density: if f : ℝ → ℝ≥0∞ is almost everywhere measurable on Ι a b with finite lower integral there, then for almost every t ∈ [a, b] the averages (∫⁻ r in Ι t s, f r) / edist s t over the intervals between t and s tend to f t as s tends to t from either side.