Lemma U: scalar path inequalities

Two elementary facts about absolutely continuous scalar paths: the Cauchy–Schwarz bound for interval integrals, and the energy balance for an integral path.

theorem AVenhance.Infra.FullTheorem.LemmaU.sq_intervalIntegral_le {f : ℝ → ℝ} {s t : ℝ} (hst : s ≤ t) (hf : IntervalIntegrable f MeasureTheory.volume s t) (hf2 : IntervalIntegrable (fun (r : ℝ) => f r ^ 2) MeasureTheory.volume s t) : (∫ (r : ℝ) in s..t, f r) ^ 2 ≤ (t - s) * ∫ (r : ℝ) in s..t, f r ^ 2

Cauchy–Schwarz for interval integrals.

theorem AVenhance.Infra.FullTheorem.LemmaU.scalar_path_energy {y q : ℝ → ℝ} {t : ℝ} (ht : 0 ≤ t) (hy : ∀ s ∈ Set.Icc 0 t, y s = y 0 - ∫ (r : ℝ) in 0..s, q r) (hq : IntervalIntegrable q MeasureTheory.volume 0 t) : ∫ (s : ℝ) in 0..t, 2 * (q s * y s) = y 0 ^ 2 - y t ^ 2

Energy balance for a scalar integral path.