Local energy estimate for a parabolic differential inequality #
This file proves the localized energy estimate in lem:caccioppoli.
theorem
ESS.localizedEnergyIdentity
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
(hΩ : IsOpen Ω)
(hI : IsOpen I)
{w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hderiv : CKN.HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw)
(hL2 :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤)
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφc : HasCompactSupport φ)
{δ₀ : ℝ}
(hδ₀ : 0 < δ₀)
(hbuffer : ∀ q ∈ tsupport φ, Metric.closedBall q (4 * δ₀) ⊆ Ω ×ˢ I)
:
(∑ i : Fin 3,
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), (Ω ×ˢ I).indicator
(fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => w (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y)) q
i * (Ω ×ˢ I).indicator
(fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => Dtw (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i * φ q) + ∑ i : Fin 3,
∑ j : Fin 3,
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), φ q * (Ω ×ˢ I).indicator
(fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => w (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i * (Ω ×ˢ I).indicator
(fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => D2w (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i j j = ((-(1 / 2) * ∑ i : Fin 3,
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), (Ω ×ˢ I).indicator
(fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
w (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 * (Ω ×ˢ I).indicator
(fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
Dw (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) * (Ω ×ˢ I).indicator
(fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => w (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i * (Ω ×ˢ I).indicator
(fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => Dw (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q i j
The local energy identity for a smooth compactly supported weight (lem:caccioppoli).