The time derivative of the regularized velocity on a time slice

At a positive time the regularized momentum right-hand side is the Laplacian minus the transport term minus the pressure gradient. The pressure gradient is bounded by the transport term in L² (lem:lps-regularized-Hk-start, the pressure equation), so the time derivative has L² norm squared at most 3 ‖∇²U_ε‖² + C ‖∇U_ε‖₂³ ‖∇²U_ε‖₂ on each slice.

theorem ESS.LPS.lps_regR12_pressure_weak (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 < t) (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRegP ρ ε hε b hb (x, t) * CKN.spatialLaplacian ψ x = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRegV ρ ε hε b hb (x, t) i * lpsRegU ρ ε hε b hb (x, t) j * CKN.mixedSecond ψ i j x

The weak form of the pressure equation of the regularized solution at a positive time (thm:regularised of the CKN manuscript, (R4)).

theorem ESS.LPS.lps_regR12_pressure_gradient_sq_le (ρ : 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), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => lpsRegP ρ ε hε b hb (y, t)) i x ^ 2 ≤ ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRegTransport ρ ε hε b hb i t x ^ 2

The pressure gradient of the regularized solution is bounded in L² by the transport term (thm:regularised of the CKN manuscript, (R4)).

theorem ESS.LPS.lps_sq_sum_three_le (a b c : ℝ) : (a + b + c) ^ 2 ≤ 3 * (a ^ 2 + b ^ 2 + c ^ 2)

The square of a sum of three real numbers is at most three times the sum of the squares.

theorem ESS.LPS.lps_regR12_transport_sq_sum_le (ρ : 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), lpsRegTransport ρ ε hε b hb i t x ^ 2 ≤ 27 * (CKN.gagliardoNirenbergSobolevConstant.toReal ^ 3 * lpsRegGradEnergy ρ ε hε b hb t ^ (3 / 2) * lpsRegHessEnergy ρ ε hε b hb t ^ (1 / 2))

The transport term of the regularized momentum equation has L² norm squared at most 27 S³ ‖∇U_ε‖₂³ ‖∇²U_ε‖₂ summed over components (prop:lps-local-strong).

theorem ESS.LPS.lps_regR12_Q_slice (ρ : 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 (fun (x : CKN.Foundation.Parabolic.Vec3) => lpsRegQ ρ ε hε b hb (x, t) i) 2 MeasureTheory.volume) ∧ ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRegQ ρ ε hε b hb (x, t) i ^ 2 ≤ 3 * lpsRegHessEnergy ρ ε hε b hb t + 162 * (CKN.gagliardoNirenbergSobolevConstant.toReal ^ 3 * lpsRegGradEnergy ρ ε hε b hb t ^ (3 / 2) * lpsRegHessEnergy ρ ε hε b hb t ^ (1 / 2))

On a positive-time slice, the time derivative of the regularized velocity is square integrable with ∑ᵢ ‖∂ₜ Uᵢ‖₂² ≤ 3 ‖∇²U_ε‖₂² + 162 S³ ‖∇U_ε‖₂³ ‖∇²U_ε‖₂ (prop:lps-local-strong).