Absorption estimate for a localized energy identity #
This module estimates the terms in the local identity from lem:caccioppoli.
theorem
ESS.caccioppoliWeightedEnergyBound
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
(hΩ : IsOpen Ω)
(hI : IsOpen I)
(r c₁ Csp Ctime : ℝ)
(hr : 0 < r)
(hc₁ : 0 ≤ c₁)
(hCsp : 0 ≤ Csp)
{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 < ⊤)
(hineq :
∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω I), (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtw z i + ∑ j : Fin 3, D2w z i j j) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) + √(CKN.spatialGradientSq w Dw z)))
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφc : HasCompactSupport φ)
{δ₀ : ℝ}
(hδ₀ : 0 < δ₀)
(hbuffer : ∀ q ∈ tsupport φ, Metric.closedBall q (4 * δ₀) ⊆ Ω ×ˢ I)
(hφrange : ∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 ≤ φ q ∧ φ q ≤ 1)
(hspatial :
∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ j : Fin 3, (fderiv ℝ φ q) (CKN.basisVec j, 0) ^ 2 ≤ Csp / r ^ 2 * φ q)
(htime : ∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), -Ctime / r ^ 2 ≤ (fderiv ℝ φ q) (0, 1))
:
have U := Ω ×ˢ I;
have W := fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
U.indicator (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => w (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q;
have D := fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
U.indicator (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => Dw (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
q;
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), φ q * ∑ i : Fin 3, ∑ j : Fin 3, D q i j ^ 2 ≤ 2 * (c₁ + c₁ ^ 2 + (Csp + Ctime / 2) / r ^ 2) * ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (W q) ^ 2
A compactly supported cutoff turns the differential inequality into a weighted
spatial energy estimate (lem:caccioppoli).