Time-localized cutoff error comparison

The singular lower-time derivative appears only in its transition strip; this support is retained when estimating the squared error.

theorem ESS.buShortCutoffHeatErrorSize_le_coeff_indicator {scale R ε c₁ m h : ℝ} (hscale : 0 < scale) (hR : 0 < R) (hε : 0 < ε) (hc₁ : 0 ≤ c₁) (hm : 0 ≤ m) (hh : 0 ≤ h) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hM : buShortSpacePhaseGradientSize scale R hR z ≤ m) (hH : buShortSpacePhaseHeatSize scale R hR z ≤ h) : buShortCutoffHeatErrorSize scale R hR ε c₁ v Dv z ≤ ((3 * (c₁ * scale) + 18) * m + h) * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z)) + if 1 / 2 + ε ≤ z.2 ∧ z.2 ≤ 1 / 2 + 2 * ε then 8 / ε * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) else 0

Bounds for the two fixed cutoff derivative sizes yield a bound for the full cutoff heat error with its lower-time support retained.

theorem ESS.buShortCutoffHeatErrorSize_pointwise_indicator {scale R ε c₁ C₁ C₂ : ℝ} (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) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hs : 1 / 2 < z.2) (hs1 : z.2 < 1) : buShortCutoffHeatErrorSize scale R ⋯ ε c₁ v Dv z ≤ (if z ∈ buShortWideGapRegion scale then buShortUniformErrorCoeff scale c₁ C₁ C₂ * (1 + z.1 2) ^ 2 else buShortShellCoeff scale R c₁) * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z)) + if 1 / 2 + ε ≤ z.2 ∧ z.2 ≤ 1 / 2 + 2 * ε then 8 / ε * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) else 0

The phase-gap or shell majorant retains the lower-time transition indicator.

theorem ESS.buShortCutoffHeatErrorSize_sq_pointwise_indicator {scale R ε c₁ C₁ C₂ : ℝ} (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) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hs : 1 / 2 < z.2) (hs1 : z.2 < 1) : buShortCutoffHeatErrorSize scale R ⋯ ε c₁ v Dv z ^ 2 ≤ (4 * 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 * (if 1 / 2 + ε ≤ z.2 ∧ z.2 ≤ 1 / 2 + 2 * ε then 8 / ε * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) else 0) ^ 2

The squared cutoff heat error separates phase, shell, and time-transition densities with the time support retained.