Integrating sliding-window integrals on the line

For f : ℝ → ℝ≥0∞ and h : ℝ, integrating the window integrals ∫⁻ r in Ioc t (t + h), f r over all t gives ENNReal.ofReal h * ∫⁻ r, f r. For 0 ≤ h this is Tonelli's theorem: the windows Ioc t (t + h) of length h cover each point of the line for a set of t of length h; for h < 0 the windows are empty and both sides vanish. Restricted to the starting points t ∈ Ioc a (b - h), whose windows lie in Ioc a b, this bounds the integrated window integrals by ENNReal.ofReal h * ∫⁻ r in Ioc a b, f r.

This is the averaging step that turns pointwise bounds of a difference quotient over a window of length h > 0 by h⁻¹ * ∫⁻ r in Ioc t (t + h), f r into a bound of its integral by ∫⁻ f.

Main results

• TauCeti.lintegral_setLIntegral_Ioc_add: ∫⁻ t, ∫⁻ r in Ioc t (t + h), f r = ENNReal.ofReal h * ∫⁻ r, f r.
• TauCeti.setLIntegral_setLIntegral_Ioc_add_le: the windows starting in Ioc a (b - h) give at most ENNReal.ofReal h * ∫⁻ r in Ioc a b, f r.

theorem TauCeti.lintegral_setLIntegral_Ioc_add {f : ℝ → ENNReal} (hf : AEMeasurable f MeasureTheory.volume) (h : ℝ) : ∫⁻ (t : ℝ), ∫⁻ (r : ℝ) in Set.Ioc t (t + h), f r = ENNReal.ofReal h * ∫⁻ (r : ℝ), f r

Integrating the integrals of f over the sliding windows Ioc t (t + h) over all starting points t gives ENNReal.ofReal h times the integral of f: for 0 ≤ h this is h times the integral, and for h < 0 the windows are empty and both sides vanish.

theorem TauCeti.setLIntegral_setLIntegral_Ioc_add_le {f : ℝ → ENNReal} {a b : ℝ} (hf : AEMeasurable f (MeasureTheory.volume.restrict (Set.Ioc a b))) (h : ℝ) : ∫⁻ (t : ℝ) in Set.Ioc a (b - h), ∫⁻ (r : ℝ) in Set.Ioc t (t + h), f r ≤ ENNReal.ofReal h * ∫⁻ (r : ℝ) in Set.Ioc a b, f r

Integrating the integrals of f over the sliding windows Ioc t (t + h) that lie in Ioc a b, that is over the starting points t ∈ Ioc a (b - h), gives at most ENNReal.ofReal h times the integral of f over Ioc a b.