Integral Cauchy bounds without dividing by the initial-data norm.

theorem AVenhance.Infra.Section4.iterate_integral_cauchy_sq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ) (hg : MeasureTheory.Integrable (fun (x : α) => g x ^ 2) μ) (hfg : MeasureTheory.Integrable (fun (x : α) => f x * g x) μ) : (∫ (x : α), f x * g x ∂μ) ^ 2 ≤ (∫ (x : α), f x ^ 2 ∂μ) * ∫ (x : α), g x ^ 2 ∂μ

Cauchy-Schwarz in squared integral form, including zero-energy factors.

theorem AVenhance.Infra.Section4.iterate_integral_pairing_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hf : MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ) (hg : MeasureTheory.Integrable (fun (x : α) => g x ^ 2) μ) (hfg : MeasureTheory.Integrable (fun (x : α) => f x * g x) μ) (hAf : ∫ (x : α), f x ^ 2 ∂μ ≤ A ^ 2) (hBg : ∫ (x : α), g x ^ 2 ∂μ ≤ B ^ 2) : |∫ (x : α), f x * g x ∂μ| ≤ A * B

Quantitative L2 bounds give a linear pairing bound, including A=0 or B=0.