Weighted cutoff error comparison #
The squared heat error of the compact short-time cutoff is bounded by its phase, shell, and lower-time majorants with no auxiliary integrability assumptions.
theorem
ESS.bu_short_weighted_error_le_split
(scale R ε c₁ C₁ C₂ a : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(hR : 1 ≤ R)
(hε : 0 < ε)
(hc₁ : 0 ≤ c₁)
(hC₁ : 0 ≤ C₁)
(hN : ∀ (scale y : ℝ), |deriv (deriv (buShortNormalCutoff scale)) y| ≤ C₁)
(hC₂ : 0 ≤ C₂)
(hP : ∀ (x : ℝ), |deriv (deriv CKN.smoothTransitionProfile) x| ≤ 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)
(hcont : ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1))
(hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw)
(hL2 :
∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1),
Bornology.IsBounded S →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤)
:
have K := buCutSupportSet (buShortFullCutoff scale R ⋯ ε);
have v := buAffineField (-scale ^ 2 / 2) scale w;
have Dv := buAffineDw (-scale ^ 2 / 2) scale Dw;
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortShiftedWeight scale a z * buShortCutoffHeatErrorSize scale R ⋯ ε c₁ v Dv z ^ 2 ≤ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, (4 * buShortShiftedWeight scale a z * if z ∈ buShortWideGapRegion scale then buShortUniformErrorCoeff scale c₁ C₁ C₂ ^ 2 * (1 + z.1 2) ^ 4
else buShortShellCoeff scale R c₁ ^ 2) * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z) + 2 * buShortShiftedWeight scale a z * (if 1 / 2 + ε ≤ z.2 ∧ z.2 ≤ 1 / 2 + 2 * ε then 8 / ε * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)
else 0) ^ 2
The integrated squared cutoff heat error obeys the phase and shell comparison for fixed short-time parameters.