The mollifier limit of the energy pairing on one time slice

On one time slice the mollified energy pairing of one velocity component is a sum of four pairings of mollified square-integrable fields. As the mollifier radius tends to zero it converges to the corresponding pairing of the unmollified fields, and it is bounded uniformly in the radius by products of slice L² norms. This is the spatial limit in eq:reg-local-energy-forced.

theorem CKN.Leray.abs_integral_mul_le_eLpNorm_two {f g : Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : |∫ (x : Foundation.Parabolic.Vec3), f x * g x| ≤ (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal * (MeasureTheory.eLpNorm g 2 MeasureTheory.volume).toReal

The Cauchy–Schwarz inequality for real square-integrable functions.

theorem CKN.Leray.toReal_eLpNorm_mul_le {X h : Foundation.Parabolic.Vec3 → ℝ} (hX : MeasureTheory.MemLp X 2 MeasureTheory.volume) (hh : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) {M : ℝ} (hM : ∀ (x : Foundation.Parabolic.Vec3), |h x| ≤ M) : (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => X x * h x) 2 MeasureTheory.volume).toReal ≤ M * (MeasureTheory.eLpNorm X 2 MeasureTheory.volume).toReal

theorem CKN.Leray.toReal_eLpNorm_leConv_leMol_le {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (n : ℕ) : (MeasureTheory.eLpNorm (leConv (leMol n) g) 2 MeasureTheory.volume).toReal ≤ (MeasureTheory.eLpNorm g 2 MeasureTheory.volume).toReal

noncomputable def CKN.Leray.leDeltaRHS (n : ℕ) (uk : Foundation.Parabolic.Vec3 → ℝ) (A : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (q G F ψ : Foundation.Parabolic.Vec3 → ℝ) (k : Fin 3) : ℝ

The mollified energy pairing of one velocity component on one time slice.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Leray.leLimit (uk : Foundation.Parabolic.Vec3 → ℝ) (Dk A : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (q G F ψ : Foundation.Parabolic.Vec3 → ℝ) (k : Fin 3) : ℝ

The limiting energy pairing of one velocity component on one time slice.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.leConv_productDeriv_eq {uk ψ : Foundation.Parabolic.Vec3 → ℝ} {Dk : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hu : MeasureTheory.MemLp uk 2 MeasureTheory.volume) (hD : ∀ (j : Fin 3), MeasureTheory.MemLp (Dk j) 2 MeasureTheory.volume) (hweak : ∀ (j : Fin 3), HasWeakPartialDerivOn Set.univ j uk (Dk j)) (n : ℕ) (j : Fin 3) : (fun (x : Foundation.Parabolic.Vec3) => leConv (spatialDeriv (leMol n) j) uk x * ψ x + leConv (leMol n) uk x * (fderiv ℝ ψ x) (basisVec j)) = fun (x : Foundation.Parabolic.Vec3) => leConv (leMol n) (Dk j) x * ψ x + leConv (leMol n) uk x * (fderiv ℝ ψ x) (basisVec j)

theorem CKN.Leray.memLp_leConv_productDeriv {uk ψ : Foundation.Parabolic.Vec3 → ℝ} {Dk : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hu : MeasureTheory.MemLp uk 2 MeasureTheory.volume) (hD : ∀ (j : Fin 3), MeasureTheory.MemLp (Dk j) 2 MeasureTheory.volume) (hweak : ∀ (j : Fin 3), HasWeakPartialDerivOn Set.univ j uk (Dk j)) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (n : ℕ) (j : Fin 3) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => leConv (spatialDeriv (leMol n) j) uk x * ψ x + leConv (leMol n) uk x * (fderiv ℝ ψ x) (basisVec j)) 2 MeasureTheory.volume

theorem CKN.Leray.memLp_productDeriv {uk ψ : Foundation.Parabolic.Vec3 → ℝ} {Dk : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hu : MeasureTheory.MemLp uk 2 MeasureTheory.volume) (hD : ∀ (j : Fin 3), MeasureTheory.MemLp (Dk j) 2 MeasureTheory.volume) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (j : Fin 3) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Dk j x * ψ x + uk x * (fderiv ℝ ψ x) (basisVec j)) 2 MeasureTheory.volume

theorem CKN.Leray.tendsto_leDeltaRHS {uk q G F ψ : Foundation.Parabolic.Vec3 → ℝ} {Dk A : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hu : MeasureTheory.MemLp uk 2 MeasureTheory.volume) (hD : ∀ (j : Fin 3), MeasureTheory.MemLp (Dk j) 2 MeasureTheory.volume) (hA : ∀ (j : Fin 3), MeasureTheory.MemLp (A j) 2 MeasureTheory.volume) (hq : MeasureTheory.MemLp q 2 MeasureTheory.volume) (hG : MeasureTheory.MemLp G 2 MeasureTheory.volume) (hF : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hweak : ∀ (j : Fin 3), HasWeakPartialDerivOn Set.univ j uk (Dk j)) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (k : Fin 3) : Filter.Tendsto (fun (n : ℕ) => leDeltaRHS n uk A q G F ψ k) Filter.atTop (nhds (leLimit uk Dk A q G F ψ k))

The mollifier limit of the energy pairing on one time slice.

theorem CKN.Leray.abs_leDeltaRHS_le {uk q G F ψ : Foundation.Parabolic.Vec3 → ℝ} {Dk A : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hu : MeasureTheory.MemLp uk 2 MeasureTheory.volume) (hD : ∀ (j : Fin 3), MeasureTheory.MemLp (Dk j) 2 MeasureTheory.volume) (hA : ∀ (j : Fin 3), MeasureTheory.MemLp (A j) 2 MeasureTheory.volume) (hq : MeasureTheory.MemLp q 2 MeasureTheory.volume) (hG : MeasureTheory.MemLp G 2 MeasureTheory.volume) (hF : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hweak : ∀ (j : Fin 3), HasWeakPartialDerivOn Set.univ j uk (Dk j)) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) {M : ℝ} (hMψ : ∀ (x : Foundation.Parabolic.Vec3), |ψ x| ≤ M) (hMd : ∀ (j : Fin 3) (x : Foundation.Parabolic.Vec3), |(fderiv ℝ ψ x) (basisVec j)| ≤ M) (n : ℕ) (k : Fin 3) : |leDeltaRHS n uk A q G F ψ k| ≤ M * ((∑ j : Fin 3, (MeasureTheory.eLpNorm (A j) 2 MeasureTheory.volume).toReal + (MeasureTheory.eLpNorm q 2 MeasureTheory.volume).toReal) * (∑ j : Fin 3, (MeasureTheory.eLpNorm (Dk j) 2 MeasureTheory.volume).toReal + (MeasureTheory.eLpNorm uk 2 MeasureTheory.volume).toReal) + (MeasureTheory.eLpNorm uk 2 MeasureTheory.volume).toReal * ((MeasureTheory.eLpNorm G 2 MeasureTheory.volume).toReal + (MeasureTheory.eLpNorm F 2 MeasureTheory.volume).toReal))

The uniform bound of the mollified energy pairing on one time slice.