Support of the lower-time derivative term

The singular coefficient in the cutoff heat error is confined to the time interval in which the lower-time cutoff changes.

theorem ESS.buShortTimeCutoff_abs_deriv_le_indicator {ε : ℝ} (hε : 0 < ε) (s : ℝ) : |deriv (buShortTimeCutoff ε) s| ≤ if 1 / 2 + ε ≤ s ∧ s ≤ 1 / 2 + 2 * ε then 8 / ε else 0

The lower-time derivative is supported in its closed transition strip.

theorem ESS.buShortCutoffHeatScalarSize_le_spacePhase_indicator (scale R ε : ℝ) (hR : 0 < R) (hε : 0 < ε) (z : CKN.Foundation.Parabolic.ParabolicPoint) : |CKN.timePartial (buCutScalar (buShortFullCutoff scale R hR ε)) z + ∑ j : Fin 3, CKN.spatialSecondPartial (buCutScalar (buShortFullCutoff scale R hR ε)) j j z| ≤ buShortSpacePhaseHeatSize scale R hR z + if 1 / 2 + ε ≤ z.2 ∧ z.2 ≤ 1 / 2 + 2 * ε then 8 / ε else 0

The scalar heat derivative contains only one term supported on the initial-time transition strip.

theorem ESS.buShortCutoffHeatErrorSize_le_spacePhase_indicator (scale R ε c₁ : ℝ) (hR : 0 < R) (hε : 0 < ε) (hscale : 0 ≤ scale) (hc₁ : 0 ≤ 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) : buShortCutoffHeatErrorSize scale R hR ε c₁ v Dv z ≤ (3 * (c₁ * scale) * buShortSpacePhaseGradientSize scale R hR z + buShortSpacePhaseHeatSize scale R hR z) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + 18 * buShortSpacePhaseGradientSize scale R hR 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 singular part of the full cutoff heat error is supported only in the initial-time transition strip.