L² continuity in time of the regularized momentum right-hand side

The pressure-free part R = Δ U_ε - (J_ε U_ε · ∇) U_ε of the regularized momentum right-hand side is continuous in time with values in L², by the continuity of the ordered derivative paths and sup-norm bounds for the mollified transport velocity (lem:lps-regularized-Hk-start).

theorem ESS.LPS.lps_regR12_word_path_continuousAt (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {a : ℝ} (ha : 0 < a) (i : Fin 3) (α : List (Fin 3)) : ContinuousAt (lpsPath (fun (s : ℝ) (x : CKN.Foundation.Parabolic.Vec3) => CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, s) i) x) ⋯) a

Every ordered spatial derivative of the regularized velocity is L²-continuous in time at positive times.

theorem ESS.LPS.lps_regR12_kernel_memLp (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : MeasureTheory.MemLp (CKN.Leray.regUniformMollifierKernel ρ ε hε) 2 MeasureTheory.volume

The mollifier kernel is square integrable.

theorem ESS.LPS.lps_regR12_V_eq_conv (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) (x : CKN.Foundation.Parabolic.Vec3) (k : Fin 3) : lpsRegV ρ ε hε b hb (x, t) k = MeasureTheory.convolution (CKN.Leray.regUniformMollifierKernel ρ ε hε) (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, t) k) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

The mollified transport velocity is the convolution of the velocity slice with the mollifier kernel.

theorem ESS.LPS.lps_regR12_V_diff_abs_le (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {r a : ℝ} (hr : 0 ≤ r) (ha : 0 ≤ a) (x : CKN.Foundation.Parabolic.Vec3) (k : Fin 3) : |lpsRegV ρ ε hε b hb (x, r) k - lpsRegV ρ ε hε b hb (x, a) k| ≤ √(∫ (y : CKN.Foundation.Parabolic.Vec3), CKN.Leray.regUniformMollifierKernel ρ ε hε y ^ 2) * √(∫ (y : CKN.Foundation.Parabolic.Vec3), (lpsRegU ρ ε hε b hb (y, r) k - lpsRegU ρ ε hε b hb (y, a) k) ^ 2)

The sup-norm distance of the mollified transport velocity at two times is bounded by the kernel's L² norm times the L² distance of the velocity slices.

theorem ESS.LPS.lps_regR12_V_abs_le (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) (x : CKN.Foundation.Parabolic.Vec3) (k : Fin 3) : |lpsRegV ρ ε hε b hb (x, t) k| ≤ √(∫ (y : CKN.Foundation.Parabolic.Vec3), CKN.Leray.regUniformMollifierKernel ρ ε hε y ^ 2) * √(∫ (y : CKN.Foundation.Parabolic.Vec3), lpsRegU ρ ε hε b hb (y, t) k ^ 2)

The mollified transport velocity is bounded by the kernel's L² norm times the L² norm of the velocity slice.

noncomputable def ESS.LPS.lpsRegTransportTerm (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (k i : Fin 3) (t : ℝ) : CKN.Foundation.Parabolic.Vec3 → ℝ

One summand V_k ∂_k U_i of the transport term.

Equations

• ESS.LPS.lpsRegTransportTerm ρ ε hε b hb k i t x = ESS.LPS.lpsRegV ρ ε hε b hb (x, t) k * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ESS.LPS.lpsRegU ρ ε hε b hb (y, t) i) k x

theorem ESS.LPS.lps_regR12_transportTerm_memLp (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) (k i : Fin 3) : MeasureTheory.MemLp (lpsRegTransportTerm ρ ε hε b hb k i t) 2 MeasureTheory.volume

Every summand of the transport term is square integrable.

theorem ESS.LPS.lps_regR12_transportTerm_continuousAt (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {a : ℝ} (ha : 0 < a) (k i : Fin 3) : ContinuousAt (lpsPath (lpsRegTransportTerm ρ ε hε b hb k i) ⋯) a

Every summand of the transport term is L²-continuous in time at positive times.

noncomputable def ESS.LPS.lpsRegLap (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (i : Fin 3) (t : ℝ) : CKN.Foundation.Parabolic.Vec3 → ℝ

The Laplacian of the i-th component of the regularized velocity.

Equations

• ESS.LPS.lpsRegLap ρ ε hε b hb i t = CKN.spatialLaplacian fun (y : CKN.Foundation.Parabolic.Vec3) => ESS.LPS.lpsRegU ρ ε hε b hb (y, t) i

noncomputable def ESS.LPS.lpsRegR (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (i : Fin 3) (t : ℝ) : CKN.Foundation.Parabolic.Vec3 → ℝ

The regularized momentum right-hand side without its pressure gradient.

Equations

• ESS.LPS.lpsRegR ρ ε hε b hb i t x = ESS.LPS.lpsRegLap ρ ε hε b hb i t x - ESS.LPS.lpsRegTransport ρ ε hε b hb i t x

theorem ESS.LPS.lps_regR12_transport_memLp (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) (i : Fin 3) : MeasureTheory.MemLp (lpsRegTransport ρ ε hε b hb i t) 2 MeasureTheory.volume

The transport term is square integrable.

theorem ESS.LPS.lps_regR12_R_memLp (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) (i : Fin 3) : MeasureTheory.MemLp (lpsRegR ρ ε hε b hb i t) 2 MeasureTheory.volume

The pressure-free momentum right-hand side is square integrable.

theorem ESS.LPS.lps_regR12_lap_path_continuousAt (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {a : ℝ} (ha : 0 < a) (i : Fin 3) : ContinuousAt (lpsPath (lpsRegLap ρ ε hε b hb i) ⋯) a

The Laplacian of the regularized velocity is L²-continuous in time at positive times.

theorem ESS.LPS.lps_regR12_transport_path_continuousAt (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {a : ℝ} (ha : 0 < a) (i : Fin 3) : ContinuousAt (lpsPath (lpsRegTransport ρ ε hε b hb i) ⋯) a

The transport term is L²-continuous in time at positive times.

theorem ESS.LPS.lps_regR12_R_path_continuousAt (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {a : ℝ} (ha : 0 < a) (i : Fin 3) : ContinuousAt (lpsPath (lpsRegR ρ ε hε b hb i) ⋯) a

The pressure-free momentum right-hand side is L²-continuous in time at positive times (lem:lps-regularized-Hk-start).