The time Cauchy estimate

An L²-in-time energy bound gives the square-root modulus needed by weak path compactness.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.two_ne_top_timeHolder : Fact (2 ≠ ⊤)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.intervalIntegral_nonneg_le_sqrt_energy {g : ℝ → ℝ} {s t E : ℝ} (hst : s ≤ t) (hs : 0 ≤ s) (ht : t ≤ 1) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ioc 0 1))) (hgnonneg : ∀ᵐ (r : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 1), 0 ≤ g r) (hE : ∫ (r : ℝ) in 0..1, g r ^ 2 ≤ E) : ∫ (r : ℝ) in s..t, g r ≤ √(t - s) * √E

On a subinterval, the integral of a nonnegative function is bounded by the square root of the interval length times its global L² energy.