The differentiated energy identity for the regularized velocity

The squared gradient norm ‖∇U_ε(t)‖₂² of the regularized velocity is differentiable at every positive time, with derivative -2‖∇²U_ε‖₂² + 2⟨(J_ε U_ε · ∇) U_ε, ΔU_ε⟩. The pressure does not enter (eq:lps-uniform-H1, lem:lps-regularized-Hk-start).

noncomputable def ESS.LPS.lpsRegNegLap (ρ : 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 → ℝ

Minus the Laplacian of the regularized velocity.

Equations

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

theorem ESS.LPS.lps_regR12_negLap_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 (lpsRegNegLap ρ ε hε b hb i t) 2 MeasureTheory.volume

Minus the Laplacian of the regularized velocity is square integrable.

theorem ESS.LPS.lps_regR12_negLap_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 (lpsRegNegLap ρ ε hε b hb i) ⋯) a

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

noncomputable def ESS.LPS.lpsRegRPath (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (i : Fin 3) : ℝ → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The L² path of the pressure-free momentum right-hand side (clamped at time zero).

Equations

• ESS.LPS.lpsRegRPath ρ ε hε b hb i = ESS.LPS.lpsPath (ESS.LPS.lpsRegR ρ ε hε b hb i) ⋯

noncomputable def ESS.LPS.lpsRegNegLapPath (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (i : Fin 3) : ℝ → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The L² path of minus the Laplacian of the regularized velocity (clamped at time zero).

Equations

• ESS.LPS.lpsRegNegLapPath ρ ε hε b hb i = ESS.LPS.lpsPath (ESS.LPS.lpsRegNegLap ρ ε hε b hb i) ⋯

theorem ESS.LPS.lps_regR12_inner_eq_Q_pairing (ρ : 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, inner ℝ (lpsRegRPath ρ ε hε b hb i r) (lpsRegNegLapPath ρ ε hε b hb i a + lpsRegNegLapPath ρ ε hε b hb i 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 pairing of the pressure-free right-hand side against -Δ(U_ε(a) + U_ε(c)) equals that of the full momentum right-hand side, because the pressure gradient is orthogonal to this solenoidal field (lem:lps-regularized-Hk-start).

theorem ESS.LPS.lps_regR12_gradient_energy_increment_any (ρ : 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) : IntervalIntegrable (fun (r : ℝ) => ∑ i : Fin 3, inner ℝ (lpsRegRPath ρ ε hε b hb i r) (lpsRegNegLapPath ρ ε hε b hb i a + lpsRegNegLapPath ρ ε hε b hb i c)) MeasureTheory.volume a c ∧ lpsRegGradEnergy ρ ε hε b hb c - lpsRegGradEnergy ρ ε hε b hb a = ∫ (r : ℝ) in a..c, ∑ i : Fin 3, inner ℝ (lpsRegRPath ρ ε hε b hb i r) (lpsRegNegLapPath ρ ε hε b hb i a + lpsRegNegLapPath ρ ε hε b hb i c)

The increment of the squared gradient norm of the regularized velocity between two positive times, in either order, is the time integral of the paired pressure-free right-hand side (prop:lps-local-strong).

theorem ESS.LPS.lps_regR12_gradient_energy_hasDerivAt (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {a : ℝ} (ha : 0 < a) : HasDerivAt (lpsRegGradEnergy ρ ε hε b hb) (2 * ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRegR ρ ε hε b hb i a x * -lpsRegLap ρ ε hε b hb i a x) a

The squared gradient norm of the regularized velocity is differentiable at every positive time, with derivative twice the pairing of the pressure-free right-hand side against -ΔU_ε (eq:lps-uniform-H1).

noncomputable def ESS.LPS.lpsRegHessEnergy (ρ : 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 second spatial derivatives of the regularized velocity at time t.

Equations

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

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

The pairing of the transport term with the Laplacian of the regularized velocity.

Equations

• ESS.LPS.lpsRegTransportPairing ρ ε hε b hb t = ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), ESS.LPS.lpsRegTransport ρ ε hε b hb i t x * ESS.LPS.lpsRegLap ρ ε hε b hb i t x

theorem ESS.LPS.lps_regR12_lap_sq_eq_hess (ρ : 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, ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRegLap ρ ε hε b hb i t x ^ 2 = lpsRegHessEnergy ρ ε hε b hb t

The squared L² norm of the Laplacian of the regularized velocity is the squared L² norm of its second derivatives.

theorem ESS.LPS.lps_regR12_gradient_energy_deriv_eq (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) : 2 * ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRegR ρ ε hε b hb i t x * -lpsRegLap ρ ε hε b hb i t x = -2 * lpsRegHessEnergy ρ ε hε b hb t + 2 * lpsRegTransportPairing ρ ε hε b hb t

The derivative of the squared gradient norm of the regularized velocity is -2‖∇²U_ε‖₂² + 2⟨(J_ε U_ε · ∇) U_ε, ΔU_ε⟩ (eq:lps-uniform-H1).