Order-two Sobolev product reduction

The H² algebra estimate reduces to the product of two first derivatives. The latter receives a quantitative whole-space L⁴ bound from the Sobolev interpolation step.

theorem ESS.lps_smooth_product_normSq_two_of_middle (M : ℝ) (hM : 0 ≤ M) (hmid : ∀ (f g : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) f → ContDiff ℝ (↑⊤) g → (∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) → (∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α g) 2 MeasureTheory.volume) → ∀ (α β : List (Fin 3)), α.length = 1 → β.length = 1 → MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => (CKN.wordDeriv α f x * CKN.wordDeriv β g x) ^ 2) MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), (CKN.wordDeriv α f x * CKN.wordDeriv β g x) ^ 2 ≤ (M * CKN.sobolevNormSqOn 2 Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ f) * CKN.sobolevNormSqOn 2 Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ g) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f g : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) f → ContDiff ℝ (↑⊤) g → (∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) → (∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α g) 2 MeasureTheory.volume) → (∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) 2 MeasureTheory.volume) ∧ (CKN.sobolevNormSqOn 2 Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) ≤ (C * CKN.sobolevNormSqOn 2 Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α f) * CKN.sobolevNormSqOn 2 Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α g

A uniform middle-split estimate for first derivatives implies the ordered whole-space H² algebra estimate (eq:lps-Hm-energy).

theorem ESS.lps_smooth_product_normSq_two : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f g : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) f → ContDiff ℝ (↑⊤) g → (∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) → (∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α g) 2 MeasureTheory.volume) → (∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) 2 MeasureTheory.volume) ∧ (CKN.sobolevNormSqOn 2 Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) ≤ (C * CKN.sobolevNormSqOn 2 Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α f) * CKN.sobolevNormSqOn 2 Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α g

Smooth multiplication is bounded in the ordered whole-space H² norm (eq:lps-Hm-energy).