Increment of the regularized gradient energy

For the regularized velocity U_ε of thm:regularised of the CKN manuscript, the increment of ‖∇U_ε‖₂² over a positive time interval is the time integral of the pairing of the momentum right-hand side against -Δ(U_ε(a) + U_ε(c)), and the pressure part of this pairing vanishes (lem:lps-regularized-Hk-start, prop:lps-local-strong).

@[reducible, inline]

noncomputable abbrev ESS.LPS.lpsRegU (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The regularized velocity of thm:regularised of the CKN manuscript for the datum b.

Equations

• ESS.LPS.lpsRegU ρ ε hε b hb = CKN.Leray.regR12Velocity ρ ε hε b hb

@[reducible, inline]

noncomputable abbrev ESS.LPS.lpsRegP (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) : CKN.Foundation.Parabolic.ParabolicPoint → ℝ

The canonical regularized pressure of thm:regularised of the CKN manuscript.

Equations

• ESS.LPS.lpsRegP ρ ε hε b hb = CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε b hb)

@[reducible, inline]

noncomputable abbrev ESS.LPS.lpsRegV (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The mollified transport velocity J_ε U_ε.

Equations

• ESS.LPS.lpsRegV ρ ε hε b hb = CKN.Leray.regUniformMollifiedVelocity ρ ε hε (ESS.LPS.lpsRegU ρ ε hε b hb)

@[reducible, inline]

noncomputable abbrev ESS.LPS.lpsRegQ (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The time derivative field of the regularized velocity.

Equations

• ESS.LPS.lpsRegQ ρ ε hε b hb z i = CKN.Leray.regR12TimeRHS ρ ε hε (ESS.LPS.lpsRegU ρ ε hε b hb) (ESS.LPS.lpsRegP ρ ε hε b hb) z i

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

The squared L² norm of the spatial gradient of the regularized velocity at time t.

Equations

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

theorem ESS.LPS.lps_regR12_slice_smooth (ρ : 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) : ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (x, t) i

Every nonnegative-time slice of the regularized velocity is smooth.

theorem ESS.LPS.lps_regR12_slice_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) (α : List (Fin 3)) : MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (x, t) i) 2 MeasureTheory.volume

Every ordered spatial derivative of a nonnegative-time slice of the regularized velocity is square integrable.

theorem ESS.LPS.lps_regR12_gradient_energy_difference (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (a c : ℝ) (ha : 0 ≤ a) (hc : 0 ≤ c) (i : Fin 3) : ∫ (x : CKN.Foundation.Parabolic.Vec3), (lpsRegU ρ ε hε b hb (x, c) i - lpsRegU ρ ε hε b hb (x, a) i) * -(CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, a) i) x + CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, c) i) x) = (∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, c) i) j x ^ 2) - ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, a) i) j x ^ 2

Change of the squared gradient norm of one velocity component between two times, as a pairing against minus the Laplacian of the sum.

theorem ESS.LPS.lps_regR12_lap_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 (CKN.spatialLaplacian fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, t) i) 2 MeasureTheory.volume

The Laplacian of every regularized velocity component slice is square integrable.

theorem ESS.LPS.lps_regR12_gradient_energy_increment (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {a c : ℝ} (ha : 0 < a) (hac : a ≤ c) : IntervalIntegrable (fun (r : ℝ) => ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRegQ ρ ε hε b hb (x, r) i * -(CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, a) i) x + CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, c) i) x)) MeasureTheory.volume a c ∧ lpsRegGradEnergy ρ ε hε b hb c - lpsRegGradEnergy ρ ε hε b hb a = ∫ (r : ℝ) in a..c, ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRegQ ρ ε hε b hb (x, r) i * -(CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, a) i) x + CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, c) i) x)

The increment of the squared gradient norm of the regularized velocity between positive times is the time integral of the pairing of the momentum right-hand side against minus the Laplacian of the sum (prop:lps-local-strong).

noncomputable def ESS.LPS.lpsRegTransport (ρ : 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 transport term (J_ε U · ∇) U_i of the regularized velocity at time t.

Equations

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

theorem ESS.LPS.lps_regR12_Q_eq (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (i : Fin 3) : lpsRegQ ρ ε hε b hb (x, t) i = CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, t) i) x - lpsRegTransport ρ ε hε b hb i t x - CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegP ρ ε hε b hb (y, t)) i x

The momentum right-hand side is the Laplacian minus the transport term minus the pressure gradient.

theorem ESS.LPS.lps_spatialDeriv_neg_add {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => -(f x + g x)) i x = -(CKN.spatialDeriv f i x + CKN.spatialDeriv g i x)

A derivative of the negative of a sum of smooth functions.

theorem ESS.LPS.lps_regR12_pressure_pairing_zero (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {a c r : ℝ} (ha : 0 ≤ a) (hc : 0 ≤ c) (hr : 0 < r) : ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegP ρ ε hε b hb (y, r)) i x * -(CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, a) i) x + CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegU ρ ε hε b hb (y, c) i) x) = 0

The pressure gradient pairs to zero with the solenoidal field -Δ(U_ε(a) + U_ε(c)) (lem:lps-regularized-Hk-start).