Local Energy Smooth

Local energy identities and limit passages for the endpoint regularity proof.

theorem ESS.localEnergyVolumeIsAddHaarMeasure : MeasureTheory.volume.IsAddHaarMeasure

noncomputable def ESS.dirDeriv (f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (v z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

Directional derivative on product spacetime.

Equations

• ESS.dirDeriv f v z = (fderiv ℝ f z) v

def ESS.spatialDir (i : Fin 3) : CKN.Foundation.Parabolic.Vec3 × ℝ

The ith spatial coordinate direction on product spacetime.

Equations

• ESS.spatialDir i = (CKN.basisVec i, 0)

def ESS.timeDir : CKN.Foundation.Parabolic.Vec3 × ℝ

The time coordinate direction on product spacetime.

Equations

• ESS.timeDir = (0, 1)

def ESS.velocitySq (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The squared Euclidean norm of a vector-valued velocity.

Equations

• ESS.velocitySq u z = ∑ i : Fin 3, u z i * u z i

theorem ESS.dirDeriv_contDiff_one {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (v : CKN.Foundation.Parabolic.Vec3 × ℝ) : ContDiff ℝ ↑1 fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => dirDeriv f v z

A directional derivative of a smooth scalar function is continuously differentiable.

theorem ESS.smoothIntegral_dirDeriv_mul_eq_neg {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑1) f) (hg : ContDiff ℝ (↑1) g) (hgc : HasCompactSupport g) (v : CKN.Foundation.Parabolic.Vec3 × ℝ) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), f z * dirDeriv g v z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), dirDeriv f v z * g z

Integration by parts in a fixed space-time direction for smooth functions when the second factor is compactly supported.

noncomputable def ESS.smoothMomentumTestIntegrand (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (R G : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ) (p : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The weak momentum integrand after substituting a smooth velocity test.

Equations

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

noncomputable def ESS.smoothEnergyTestIntegrand (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (R G : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ) (p ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The expanded energy integrand after the smooth velocity test substitution.

Equations

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

def ESS.smoothVelocityTest (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3

The velocity test field 2 ψ u used in the smooth local energy identity.

Equations

• ESS.smoothVelocityTest u ψ = (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => 2 * ψ z) • u

theorem ESS.smoothMomentum_tested_energy {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) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hweak : ∀ (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ tsupport ψ → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), smoothMomentumTestIntegrand u R G p φ z = 0) (hgrad : ∀ z ∈ tsupport ψ, ∀ (i j : Fin 3), dirDeriv (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => u y i) (spatialDir j) z = G z i j) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), smoothEnergyTestIntegrand u R G p ψ z = 0

Testing a smooth momentum identity with twice the velocity times a compact scalar test produces the expanded energy identity.

noncomputable def ESS.smoothEnergyBaseIntegrand (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (R G : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ) (p ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The base energy density produced from a smooth momentum identity after collecting the velocity, pressure, stress, and gradient terms.

Equations

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

noncomputable def ESS.smoothEnergyTotalDerivative (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The total derivative terms in the smooth energy test identity.

Equations

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

theorem ESS.smoothEnergyTestIntegrand_eq_base_add_totalDerivative {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) (hψ : ContDiff ℝ (↑⊤) ψ) (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 × ℝ) (hz : z ∈ tsupport ψ) : smoothEnergyTestIntegrand u R G p ψ z = smoothEnergyBaseIntegrand u R G p ψ z + smoothEnergyTotalDerivative u ψ z

The smooth energy test density is the sum of its base density and a total derivative.