Whole-space transport pairing

The ordered transport energy pairs a derivative of the velocity with a derivative of the transport tensor. This file gives the scalar L² pairing estimate used before summing the ordered derivative words.

theorem ESS.lps_integral_pairing_le (f g : CKN.Foundation.Parabolic.Vec3 → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), f x * g x ≤ √(∫ (x : CKN.Foundation.Parabolic.Vec3), f x ^ 2) * √(∫ (x : CKN.Foundation.Parabolic.Vec3), g x ^ 2)

A whole-space L² pairing is bounded by the product of the square roots of its two squared integrals (eq:lps-regularized-Hm-identity).

theorem ESS.lps_finset_integral_pairing_le {ι : Type u_1} (s : Finset ι) (F G : ι → CKN.Foundation.Parabolic.Vec3 → ℝ) (hF : ∀ i ∈ s, MeasureTheory.MemLp (F i) 2 MeasureTheory.volume) (hG : ∀ i ∈ s, MeasureTheory.MemLp (G i) 2 MeasureTheory.volume) : ∑ i ∈ s, ∫ (x : CKN.Foundation.Parabolic.Vec3), F i x * G i x ≤ √(∑ i ∈ s, ∫ (x : CKN.Foundation.Parabolic.Vec3), F i x ^ 2) * √(∑ i ∈ s, ∫ (x : CKN.Foundation.Parabolic.Vec3), G i x ^ 2)

A finite sum of whole-space L² pairings is bounded by the square roots of the two summed energies (eq:lps-regularized-Hm-identity).