RelativeError: averaging the transport duality bound

The analytic part of the low-mode trace argument is isolated here. The remaining flow/Piola work must supply the pointwise duality inequality and its two Cauchy--Schwarz bounds.

theorem AVenhance.Infra.Section5.RelativeError.TraceAveraging.intervalIntegral_f_le_sqrt_length_mul_l2 {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc 0 1)) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : ∫ (s : ℝ) in 0..t, f s ≤ √t * √(∫ (s : ℝ) in 0..1, f s ^ 2)

theorem AVenhance.Infra.Section5.RelativeError.lowModeTrace_from_transportDuality_average {ν K T G S : ℝ} {f : ℝ → ℝ} (hν : 0 < ν) (hK : 0 < K) (hT : 0 < T) (hTle : T ≤ 1) (hTdef : T = (ν * K ^ 2)⁻¹) (_hS : 0 ≤ S) (hf : ContinuousOn f (Set.Icc 0 1)) (haverage : ∫ (t : ℝ) in 0..T, f t ≤ √T * S) (hprefix : ∀ t ∈ Set.Icc 0 T, ∫ (s : ℝ) in 0..t, f s ≤ √T * S) (hdual : ∀ t ∈ Set.Icc 0 T, G ≤ Real.exp 1 * f t + Real.exp 1 * ν * K ^ 2 * ∫ (s : ℝ) in 0..t, f s) : G ≤ 2 * Real.exp 1 * K * √ν * S

Average the transport-duality inequality on the short interval whose length is (ν K²)⁻¹. The two displayed square-root integral bounds are the Cauchy--Schwarz inputs on [0,T] and [0,t].

theorem AVenhance.Infra.Section5.RelativeError.lowModeTrace_from_transportDuality {ν K T G : ℝ} {f : ℝ → ℝ} (hν : 0 < ν) (hK : 0 < K) (hT : 0 < T) (hTle : T ≤ 1) (hTdef : T = (ν * K ^ 2)⁻¹) (hf : ContinuousOn f (Set.Icc 0 1)) (hdual : ∀ t ∈ Set.Icc 0 T, G ≤ Real.exp 1 * f t + Real.exp 1 * ν * K ^ 2 * ∫ (s : ℝ) in 0..t, f s) : G ≤ 2 * Real.exp 1 * K * √ν * √(∫ (s : ℝ) in 0..1, f s ^ 2)

Cauchy--Schwarz supplies both segment bounds needed by the averaged transport-duality estimate from the full time-interval L² norm.