Weak heat inequality for the compact short-time field #
The scaled differential inequality and scalar product rule give a pointwise almost-everywhere bound for the compact cutoff field.
noncomputable def
ESS.buShortCutoffGradientSize
(scale R : ℝ)
(hR : 0 < R)
(ε : ℝ)
(z : CKN.Foundation.Parabolic.ParabolicPoint)
:
The spatial cutoff derivative size at a parabolic point.
Equations
- ESS.buShortCutoffGradientSize scale R hR ε z = ∑ j : Fin 3, |CKN.spatialPartial (ESS.buCutScalar (ESS.buShortFullCutoff scale R hR ε)) j z|
Instances For
theorem
ESS.bu_short_cutoff_heat_ae_bound
(scale R ε c₁ : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(hR : 0 < R)
(hc₁ : 0 ≤ c₁)
(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)
(hineq :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (√(CKN.spatialGradientSq w Dw z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (w z)))
:
have κ := buShortFullCutoff scale R hR ε;
have v := buAffineField (-scale ^ 2 / 2) scale w;
have Dv := buAffineDw (-scale ^ 2 / 2) scale Dw;
have D2v := buAffineD2w (-scale ^ 2 / 2) scale D2w;
have Dtv := buAffineDtw (-scale ^ 2 / 2) scale Dtw;
have W := buCutField κ v;
have DW := buCutDw κ v Dv;
have D2W := buCutD2 κ v Dv D2v;
have DtW := buCutDt κ v Dtv;
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) 1)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2W DtW z) ≤ c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (W z) + 3 * √(CKN.spatialGradientSq W DW z)) + (3 * (c₁ * scale) * buShortCutoffGradientSize scale R hR ε z + |CKN.timePartial (buCutScalar κ) z + ∑ j : Fin 3, CKN.spatialSecondPartial (buCutScalar κ) j j z|) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + 18 * buShortCutoffGradientSize scale R hR ε z * √(CKN.spatialGradientSq v Dv z)
The weak heat vector of the compact short-time field obeys the scaled inequality plus explicit scalar cutoff errors.