The energy balance for the gradient of a strong solution #
Testing the strong form of the equation against Δu ∈ J at almost every time
and using the chain rule for ‖∇u‖² gives
d/dt ‖∇u‖² + 2‖Δu‖² = 2 ∫ (u·∇)u · Δu (lem:lps-H1-estimate).
theorem
ESS.lps_h1_energy_balance
{t₀ t₁ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hU : IsLpsStrongSolution t₀ t₁ u Du p)
(hD : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ t₁) u Du D2u Dtu)
(hMD2 : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))))
(hMDt : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))))
(hIdentity :
∀ (s t : ℝ),
s ∈ Set.Icc t₀ t₁ →
t ∈ Set.Icc t₀ t₁ →
s ≤ t →
∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t) i j ^ 2 = (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, s) i j ^ 2) - 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, Dtu z i * ∑ j : Fin 3, D2u z i j j)
:
AbsolutelyContinuousOnInterval
(fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t) i j ^ 2) t₀ t₁ ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ t₁), deriv (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t) i j ^ 2) t + 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, D2u (x, t) i j j) ^ 2 = 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, u (x, t) j * Du (x, t) i j) * ∑ j : Fin 3, D2u (x, t) i j j
The energy balance of lem:lps-H1-estimate: the gradient energy is
absolutely continuous and, almost everywhere,
d/dt ‖∇u‖² + 2‖Δu‖² = 2 ∫ (u·∇)u · Δu.