Ordered energy of a regularized velocity slice #
The physical mollifier, pointwise solenoidality, and divergence form
identify every spatial term of the high-order regularized energy
identity. The time-chain identity is supplied by its L² trajectory.
theorem
ESS.lps_regR12_ordered_energy_identity_of_time_chain
(m : ℕ)
(ρ : CKN.Leray.RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(t E' : ℝ)
(hJ : CKN.IsInJ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t))
(hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i)
(hp : ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t))
(huL2 :
∀ (i : Fin 3) (α : List (Fin 3)),
MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume)
(hpL2 :
∀ (α : List (Fin 3)),
MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t)) 2 MeasureTheory.volume)
(hchain :
E' = 2 * ∑ i : Fin 3,
∑ α ∈ CKN.sobolevWords m,
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x * CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12TimeRHS ρ ε hε u p (y, t) i)
x)
:
E' + 2 * ∑ i : Fin 3,
∑ α ∈ CKN.sobolevWords m,
∑ j : Fin 3,
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x ^ 2 = 2 * ∑ i : Fin 3,
∑ α ∈ CKN.sobolevWords m,
∑ j : Fin 3,
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x * CKN.wordDeriv α
(fun (y : CKN.Foundation.Parabolic.Vec3) =>
CKN.Leray.regUniformMollifiedVelocity ρ ε hε u (y, t) j * u (y, t) i)
x
The actual regularized momentum right-hand side satisfies the exact
ordered energy identity once its L² time-chain identity is known
(eq:lps-regularized-Hm-identity).
theorem
ESS.lps_regR12_corrected_energy_of_time_chain
(m : ℕ)
(hm : 2 ≤ m)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε)
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (t E' : ℝ),
(CKN.IsInJ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) →
(∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) →
(ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t)) →
(∀ (i : Fin 3) (α : List (Fin 3)),
MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) 2
MeasureTheory.volume) →
(∀ (α : List (Fin 3)),
MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t)) 2
MeasureTheory.volume) →
E' = 2 * ∑ i : Fin 3,
∑ α ∈ CKN.sobolevWords m,
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x * CKN.wordDeriv α
(fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12TimeRHS ρ ε hε u p (y, t) i)
x →
E' + ∑ i : Fin 3,
∑ α ∈ CKN.sobolevWords m,
∑ j : Fin 3,
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x ^ 2 ≤ C * (∑ i : Fin 3,
CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) =>
CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) ^ 2
The regularized momentum equation obeys the corrected high-order
energy inequality with a constant independent of the mollifier scale,
provided its L² time-chain identity holds (eq:lps-Hm-energy).