Local Energy Momentum Equation #
Local energy identities and limit passages for the endpoint regularity proof.
theorem
ESS.smoothMomentumEquation_tested
{u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
{F G : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ}
{p : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
(hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i)
(hF : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => F z i j)
(hG : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => G z i j)
(hp : ContDiff ℝ (↑⊤) p)
(hφ : ContDiff ℝ (↑⊤) φ)
(hφc : HasCompactSupport φ)
(hmom :
∀ z ∈ tsupport φ,
∀ (i : Fin 3),
dirDeriv (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => u y i) timeDir z + ∑ j : Fin 3, dirDeriv (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => F y i j) (spatialDir j) z - ∑ j : Fin 3, dirDeriv (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => G y i j) (spatialDir j) z + dirDeriv p (spatialDir i) z = 0)
:
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), smoothMomentumTestIntegrand u (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) => F z i j - u z i * u z j)
G p φ z = 0
A smooth momentum equation gives its weak integral identity for compactly supported smooth vector tests.
theorem
ESS.smoothEnergyTestIntegrand_integral_eq_base
{u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
{R G : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ}
{p ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i)
(hR : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => R z i j)
(hG : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => G z i j)
(hp : ContDiff ℝ (↑⊤) p)
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
(hgrad :
∀ z ∈ tsupport ψ,
∀ (i j : Fin 3), dirDeriv (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => u y i) (spatialDir j) z = G z i j)
(hdiv : ∀ z ∈ tsupport ψ, ∑ i : Fin 3, G z i i = 0)
:
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), smoothEnergyTestIntegrand u R G p ψ z = ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), smoothEnergyBaseIntegrand u R G p ψ z
Integrating the smooth energy test density removes its total derivative terms.