Integrated squared cutoff error #
The pointwise phase and shell error split passes through the compact support integral with the shifted Carleman weight.
theorem
ESS.bu_short_weighted_error_integral_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₂)
(v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(hleft :
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
buShortShiftedWeight scale a z * buShortCutoffHeatErrorSize scale R ⋯ ε c₁ v Dv z ^ 2)
(buCutSupportSet (buShortFullCutoff scale R ⋯ ε)) MeasureTheory.volume)
(hright :
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
(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)
(buCutSupportSet (buShortFullCutoff scale R ⋯ ε)) MeasureTheory.volume)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in buCutSupportSet (buShortFullCutoff scale R ⋯ ε), buShortShiftedWeight scale a z * buShortCutoffHeatErrorSize scale R ⋯ ε c₁ v Dv z ^ 2 ≤ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in buCutSupportSet (buShortFullCutoff scale R ⋯ ε), (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 squared cutoff error is dominated by its integrated phase, shell, and lower-time majorant.