The transport pairing of the regularized H¹ estimate

The pairing ⟨(J_ε U_ε · ∇) U_ε, ΔU_ε⟩ of the regularized velocity is bounded by C ‖∇U_ε‖₂^{3/2} ‖∇²U_ε‖₂^{3/2} with an absolute constant, by Hölder's inequality with exponents (6, 3, 2), interpolation of ∇U_ε between L² and L⁶, and the homogeneous H¹ → L⁶ inequality (eq:lps-uniform-H1).

theorem ESS.LPS.lps_eLpNorm_three_le_two_six {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) : MeasureTheory.eLpNorm f 3 MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 2 MeasureTheory.volume ^ (1 / 2) * MeasureTheory.eLpNorm f 6 MeasureTheory.volume ^ (1 / 2)

Interpolation between the whole-space L² and L⁶ norms at the L³ exponent (eq:lps-uniform-H1).

theorem ESS.LPS.lps_eLpNorm_mul_two_le {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) : MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 6 MeasureTheory.volume * MeasureTheory.eLpNorm g 3 MeasureTheory.volume

Hölder's inequality for a product in L², with exponents 6 and 3 (eq:lps-uniform-H1).

theorem ESS.LPS.lps_eLpNorm_two_toReal {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal = √(∫ (x : CKN.Foundation.Parabolic.Vec3), f x ^ 2)

The L² norm of a square-integrable function is the square root of its integral of squares.

theorem ESS.LPS.lps_smooth_eLpNorm_six_le {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hgd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv g k) 2 MeasureTheory.volume) : MeasureTheory.eLpNorm g 6 MeasureTheory.volume ≤ CKN.gagliardoNirenbergSobolevConstant * MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm fun (k : Fin 3) => CKN.spatialDeriv g k x) 2 MeasureTheory.volume

The homogeneous H¹ → L⁶ inequality for a smooth function with square-integrable value and gradient.

theorem ESS.LPS.lps_gradNorm_memLp_and_integral {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv g k) 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm fun (k : Fin 3) => CKN.spatialDeriv g k x) 2 MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (k : Fin 3) => CKN.spatialDeriv g k x) ^ 2 = ∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv g k x ^ 2

The Euclidean norm of the gradient of a smooth function with square-integrable gradient is square integrable, with the expected integral of squares.

theorem ESS.LPS.lps_smooth_memLp_six {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hgd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv g k) 2 MeasureTheory.volume) : MeasureTheory.MemLp g 6 MeasureTheory.volume

A smooth function with square-integrable value and gradient lies in L⁶.

theorem ESS.LPS.lps_smooth_six_toReal_le {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hgd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv g k) 2 MeasureTheory.volume) : (MeasureTheory.eLpNorm g 6 MeasureTheory.volume).toReal ≤ CKN.gagliardoNirenbergSobolevConstant.toReal * √(∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv g k x ^ 2)

Real-valued form of the H¹ → L⁶ inequality: ‖g‖₆ ≤ S (∑ₖ ‖∂ₖ g‖₂²)^{1/2}.

theorem ESS.LPS.lps_transport_term_le {V d L : CKN.Foundation.Parabolic.Vec3 → ℝ} (hV : ContDiff ℝ (↑⊤) V) (hV2 : MeasureTheory.MemLp V 2 MeasureTheory.volume) (hVd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv V k) 2 MeasureTheory.volume) (hd : ContDiff ℝ (↑⊤) d) (hd2 : MeasureTheory.MemLp d 2 MeasureTheory.volume) (hdd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv d k) 2 MeasureTheory.volume) (hL : MeasureTheory.MemLp L 2 MeasureTheory.volume) : |∫ (x : CKN.Foundation.Parabolic.Vec3), V x * d x * L x| ≤ CKN.gagliardoNirenbergSobolevConstant.toReal * √(∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv V k x ^ 2) * (√(∫ (x : CKN.Foundation.Parabolic.Vec3), d x ^ 2) ^ (1 / 2) * (CKN.gagliardoNirenbergSobolevConstant.toReal * √(∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv d k x ^ 2)) ^ (1 / 2)) * √(∫ (x : CKN.Foundation.Parabolic.Vec3), L x ^ 2)

Hölder bound for one summand of the transport pairing (eq:lps-uniform-H1).

theorem ESS.LPS.lps_core_rpow {S y h : ℝ} (hS : 0 ≤ S) (hy : 0 ≤ y) (hh : 0 ≤ h) : S * √y * (√y ^ (1 / 2) * (S * √h) ^ (1 / 2)) * √h = S ^ (3 / 2) * y ^ (3 / 4) * h ^ (3 / 4)

Exponent bookkeeping for the transport bound.

theorem ESS.LPS.lps_transport_term_le' {V d L : CKN.Foundation.Parabolic.Vec3 → ℝ} (hV : ContDiff ℝ (↑⊤) V) (hV2 : MeasureTheory.MemLp V 2 MeasureTheory.volume) (hVd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv V k) 2 MeasureTheory.volume) (hd : ContDiff ℝ (↑⊤) d) (hd2 : MeasureTheory.MemLp d 2 MeasureTheory.volume) (hdd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv d k) 2 MeasureTheory.volume) (hL : MeasureTheory.MemLp L 2 MeasureTheory.volume) {y0 h0 : ℝ} (hy : 0 ≤ y0) (hh : 0 ≤ h0) (h1 : ∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv V k x ^ 2 ≤ y0) (h2 : ∫ (x : CKN.Foundation.Parabolic.Vec3), d x ^ 2 ≤ y0) (h3 : ∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv d k x ^ 2 ≤ h0) (h4 : ∫ (x : CKN.Foundation.Parabolic.Vec3), L x ^ 2 ≤ h0) : |∫ (x : CKN.Foundation.Parabolic.Vec3), V x * d x * L x| ≤ CKN.gagliardoNirenbergSobolevConstant.toReal ^ (3 / 2) * y0 ^ (3 / 4) * h0 ^ (3 / 4)

The transport summand is bounded by S^{3/2} y^{3/4} h^{3/4} once the norms of V, d, L are bounded by y and h (eq:lps-uniform-H1).

theorem ESS.LPS.lps_regR12_V_smooth_memLp (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) : (∀ (k : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => lpsRegV ρ ε hε b hb (x, t) k) ∧ ∀ (k : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => lpsRegV ρ ε hε b hb (x, t) k) 2 MeasureTheory.volume

The mollified transport velocity has smooth components with all ordered derivatives square integrable.

theorem ESS.LPS.lps_regR12_V_grad_contraction (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) (k j : Fin 3) : ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegV ρ ε hε b hb (y, t) k) j x ^ 2 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, t) k) j x ^ 2

The mollification does not increase the L² norm of a first derivative of the velocity.

theorem ESS.LPS.lps_regR12_transportPairing_le (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) : |lpsRegTransportPairing ρ ε hε b hb t| ≤ 9 * (CKN.gagliardoNirenbergSobolevConstant.toReal ^ (3 / 2) * lpsRegGradEnergy ρ ε hε b hb t ^ (3 / 4) * lpsRegHessEnergy ρ ε hε b hb t ^ (3 / 4))

The transport pairing of the regularized velocity is bounded by 9 S^{3/2} ‖∇U_ε‖₂^{3/2} ‖∇²U_ε‖₂^{3/2} with an absolute constant (eq:lps-uniform-H1).