Local energy identity for a strong solution #
The compactly supported identity supplies the local kinetic-energy step for
prop:lps-local-strong. The strong right L² trace follows from continuity
and an a.e. initial representative.
theorem
ESS.LPS.lps_strong_velocity_energy_continuousOn
{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 → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
:
Strong L² continuity of the velocity in a strong solution makes its
fixed-time kinetic-energy representative continuous up to both endpoints
(prop:lps-local-strong).
theorem
ESS.LPS.lps_strong_gradient_energy_continuousOn
{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 → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
:
Strong L² continuity of the specified gradient gives continuity of its
fixed-time squared norm, with the same ordered component convention as
prop:lps-local-strong.
theorem
ESS.LPS.lps_strong_solution_derivative_data
{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 → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
:
∃ (D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtu :
CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3),
CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu ∧ MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))) ∧ MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))) ∧ MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))) ∧ MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))
The open-slab derivative witnesses already contained in a strong solution
(prop:lps-local-strong).
theorem
ESS.LPS.lps_l2_trace_of_ae_initial
{t₀ T : ℝ}
{b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : ℝ → CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hT : t₀ < T)
(hCont :
∀ t ∈ Set.Icc t₀ T,
Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u s x - u t x) 2 MeasureTheory.volume)
(nhdsWithin t (Set.Icc t₀ T)) (nhds 0))
(hTrace : u t₀ =ᵐ[MeasureTheory.volume] b)
:
Filter.Tendsto
(fun (t : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (t₀ + t) x - b x) 2 MeasureTheory.volume)
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
Strong L² continuity identifies any prescribed a.e. initial slice with
the strong right trace (prop:lps-local-strong).
theorem
ESS.LPS.lps_strong_localized_energy_identity
{t₀ T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hDerivs : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu)
(hL2 :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 + ‖D2u z‖ₑ ^ 2 + ‖Dtu z‖ₑ ^ 2 < ⊤)
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφc : HasCompactSupport φ)
{δ₀ : ℝ}
(hδ₀ : 0 < δ₀)
(hbuffer : ∀ q ∈ tsupport φ, Metric.closedBall q (4 * δ₀) ⊆ Set.univ ×ˢ Set.Ioo t₀ T)
:
(∑ i : Fin 3,
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)).indicator
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i * (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)).indicator
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
Dtu (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i * φ q) + ∑ i : Fin 3,
∑ j : Fin 3,
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), φ q * (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)).indicator
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i * (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)).indicator
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
D2u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i j j = ((-(1 / 2) * ∑ i : Fin 3,
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)).indicator
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i ^ 2 * (fderiv ℝ φ q) (0, 1)) - ∑ i : Fin 3,
∑ j : Fin 3,
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), φ q * (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)).indicator
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
Du (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i j ^ 2) - ∑ i : Fin 3,
∑ j : Fin 3,
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), (fderiv ℝ φ q) (CKN.basisVec j, 0) * (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)).indicator
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i * (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)).indicator
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
Du (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i j
The localized kinetic-energy identity with a compact space-time weight
(prop:lps-local-strong).