Averages of a moving window integral

prop:lps-smoothing: the initial-layer control of the time-difference quotients. For a nonnegative integrable f, the mean over [a,a+δ] of the window averages (1/h) ∫_τ^{τ+h} f is at most ∫_a^{a+δ+h} f (Fubini for the sliding window).

theorem ESS.LPS.lps_window_average_integral_le {a δ h : ℝ} (hδ : 0 < δ) (hh : 0 < h) {f : ℝ → ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a (a + δ + h)) (hf0 : ∀ x ∈ Set.Icc a (a + δ + h), 0 ≤ f x) : ∫ (τ : ℝ) in a..a + δ, 1 / h * ∫ (σ : ℝ) in τ..τ + h, f σ ≤ ∫ (σ : ℝ) in a..a + δ + h, f σ

The integral over [a, a+δ] of window averages of a nonnegative integrable function is at most the integral over the enlarged interval (prop:lps-smoothing).