Interval integrals dominated by a hyperbolic cosine #
An integrand dominated by C * cosh (k * t) has a primitive bounded by
C * cosh (k * t) / k for k > 0, in either time direction. This estimate controls
Picard iteration in a weighted space of bounded continuous functions on the whole real line.
theorem
TauCeti.norm_intervalIntegral_le_cosh
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{k C : ℝ}
(hk : 0 < k)
(hC : 0 ≤ C)
{F : ℝ → E}
(t : ℝ)
(hF : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.uIoc 0 t), ‖F s‖ ≤ C * Real.cosh (k * s))
:
A hyperbolic-cosine bound on an integrand gives a hyperbolic-cosine bound on its interval integral from zero, for either sign of the endpoint. Only an almost-everywhere bound on the interval of integration is required.