Gaussian average bounds for local gradient energy #
A Gaussian averaging box dominates the outer Caccioppoli cylinder of a short-time dyadic cell.
theorem
ESS.bu_short_average_gradient_bound
(X : CKN.Foundation.Parabolic.Vec3)
(δ c : ℝ)
(hδ : 0 < δ)
(hδhalf : δ < 1 / 2)
(hc : 0 ≤ c)
(hball : CKN.Foundation.Parabolic.vec3Ball X (2 * (√δ / 8)) ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2})
(havgBall : CKN.Foundation.Parabolic.vec3Ball X √(3 * δ / 2) ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2})
{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}
(hcont : ContinuousOn v ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico (1 / 2) (3 / 2)))
(hweak :
CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2)) v Dv D2v Dtv)
(hlocal :
∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2)),
Bornology.IsBounded S →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤)
(hineq :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2))), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c * (√(CKN.spatialGradientSq v Dv z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)))
:
have r := √δ / 8;
have t := 1 / 2 + δ - r ^ 2 / 2;
have Avg :=
CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball X √(3 * δ / 2)) (Set.Ioo (1 / 2 + δ / 2) (1 / 2 + 5 * δ / 4));
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball X r) (Set.Ioo t (t + r ^ 2)), CKN.spatialGradientSq v Dv z ≤ 256 * (1 + c ^ 2 + 1 / r ^ 2) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in Avg, CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2
The Gaussian velocity average bounds gradient energy in the inner
Caccioppoli cylinder (lem:bu-small-time).