Pointwise Bound by an Interval Average

This auxiliary lemma gives a mean-value bound for an integrable real function.

Let $T>0$ and let $f:\mathbb R\to\mathbb R$ be integrable on $(T,2T]$. Then there exists $t\in[T,2T]$ such that

The lemma is a technical interval-averaging fact used to select a time with controlled energy.

Formalization Note. Integrability is required only for the restriction of $f$ to $(T,2T]$; the selected point lies in the closed interval $[T,2T]$.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

private theorem exists_le_setIntegral_div
    {f : ℝ → ℝ} {T : ℝ} (hT : 0 < T)
    (hf : Integrable f (volume.restrict (Set.Ioc T (2 * T)))) :
    ∃ t ∈ Set.Icc T (2 * T),
      f t ≤ (∫ s in Set.Ioc T (2 * T), f s) / T

Module navigation

Module: KLS/BKL/Localization/CutoffEnergy/Boundary.

Next: IsEldanCutoff.integral_energy_le_weighted_add.

Source excerpt, lines 76–80 · Frozen source 408915f.