The elliptic Cauchy-Schwarz bound of eq:aniso:closure:mixed:bound

This file proves the third piece of the elliptic Cauchy-Schwarz step that feeds into the mixed term bound eq:aniso:closure:mixed:bound: the classical L² Cauchy-Schwarz inequality splits the two second-derivative-carrying summands of eq:aniso:closure:mixed by ∫|f g| ≤ √(∫f²) √(∫g²). The caller supplies the elliptic bounds ‖χ ∇b‖ ≤ C √(Y+1) and ‖χ ∇²b‖ ≤ C √(M+1) as hY, hM, hY1, hM1.

theorem CIV.abs_integral_mul_le_sqrt_mul_sqrt {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)

The Cauchy-Schwarz inequality for the Bochner integral on Vec3, in the square-root form used by the comparison energy estimate.

theorem CIV.abs_integral_cutoff_sq_secondPartial_mul_curl_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} {t Y M : ℝ} (hf : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => χ x * CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 2 (x, t)) 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => χ x * curlComp u 2 (x, t)) 2 MeasureTheory.volume) (hM : ∫ (x : CKN.Foundation.Parabolic.Vec3), (χ x * CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 2 (x, t)) ^ 2 ≤ M + 1) (hY : ∫ (x : CKN.Foundation.Parabolic.Vec3), (χ x * curlComp u 2 (x, t)) ^ 2 ≤ Y) : |∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 2 (x, t) * curlComp u 2 (x, t)| ≤ √(M + 1) * √Y

The elliptic Cauchy-Schwarz bound for the z-derivative term of eq:aniso:closure:mixed. The second-derivative factor is χ · ∂_z² u_z and the first-derivative factor is χ · (curl u)_z; Cauchy-Schwarz gives ∫ χ² (∂_z² u_z) ((curl u)_z) ≤ √(M+1) √Y.

theorem CIV.abs_integral_cutoff_sq_firstPartial_mul_dzcurl_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} {t Y M : ℝ} (hf : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => χ x * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 (x, t)) 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => χ x * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => curlComp u 2 w) 2 (x, t)) 2 MeasureTheory.volume) (hY1 : ∫ (x : CKN.Foundation.Parabolic.Vec3), (χ x * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 (x, t)) ^ 2 ≤ Y + 1) (hM1 : ∫ (x : CKN.Foundation.Parabolic.Vec3), (χ x * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => curlComp u 2 w) 2 (x, t)) ^ 2 ≤ M) : |∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 (x, t) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => curlComp u 2 w) 2 (x, t)| ≤ √(Y + 1) * √M

The elliptic Cauchy-Schwarz bound for the r-derivative term of eq:aniso:closure:mixed. The first-derivative factor is χ · ∂_r u_z and the z-derivative-of-curl factor is χ · ∂_z (curl u)_z; Cauchy-Schwarz gives ∫ χ² (∂_r u_z) (∂_z (curl u)_z) ≤ √(Y+1) √M.