Weighted energy on the Gaussian transition shell #
The collar cover, time grid, and local Caccioppoli estimate combine to bound the weighted gradient energy by the weighted radial mass.
noncomputable def
ESS.buGaussianRadialWeightedMass
(ρ a : ℝ)
(v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
:
The Gaussian-weighted square of a field restricted to the radial region
needed for the collar estimate (eq:bu-gaussian-collar).
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
ESS.buGaussianShellInnerCell
(r : ℝ)
(p : (Fin (Besicovitch.multiplicity CKN.BUGaussianSpace) × CKN.Foundation.Parabolic.Vec3) × ℕ)
:
The inner localization cylinder at a spatial center and time-grid index.
Equations
- ESS.buGaussianShellInnerCell r p = CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball p.1.2 r) (ESS.buGaussianTimeGridInner (1 / 6) (r ^ 2) p.2)
Instances For
def
ESS.buGaussianShellOuterCell
(r : ℝ)
(p : (Fin (Besicovitch.multiplicity CKN.BUGaussianSpace) × CKN.Foundation.Parabolic.Vec3) × ℕ)
:
The larger localization cylinder surrounding the corresponding inner cell.
Equations
- ESS.buGaussianShellOuterCell r p = CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball p.1.2 (2 * r)) (ESS.buGaussianTimeGridOuter (1 / 6) (r ^ 2) p.2)
Instances For
theorem
ESS.buGaussian_transition_shell_gradient_caccioppoli
{ρ a r c : ℝ}
(hρ : 4 < ρ)
(ha : 0 < a)
(hr : 0 < r)
(hrle : r ≤ 1 / 16)
(hc : 0 ≤ c)
{v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2) v Dv D2v Dtv)
(hcont : ContinuousOn v (CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ico (1 / 6) 2))
(hL2 :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2), ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤)
(hineq :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z)))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet
{y : CKN.Foundation.Parabolic.Vec3 | 13 * ρ / 20 ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm y ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm y ≤ 3 * ρ / 4}
(Set.Ioo (1 / 6) (23 / 12)), ucGaussianWeight a z * CKN.spatialGradientSq v Dv z ≤ Real.exp (2 * (56 * a * (2 * r) ^ 2 + 12 * ρ * (2 * r) + 36 * ρ ^ 2 * (2 * r) ^ 2)) * (256 * (1 + c ^ 2 + 1 / (2 * r / 2) ^ 2)) * (8 * ↑(Besicovitch.multiplicity CKN.BUGaussianSpace) ^ 2) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2), buGaussianRadialWeightedMass ρ a v z
Caccioppoli on the finitely many collar cells bounds the transition-shell
gradient by the weighted radial mass. (eq:bu-gaussian-collar)