Heat operator on the Gaussian cutoff plateau

All cutoff derivatives vanish in the interior after the initial time transition, leaving the original weak heat operator.

theorem ESS.ucGaussianCutoff_heat_eq_on_inner {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucInnerRegion ρ) (v : 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) : ucCutoffHeat (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dw D2w Dtw z = ucInitialTimeCutoff ε z.2 • ucWeakHeatVector D2w Dtw z + deriv (ucInitialTimeCutoff ε) z.2 • v z

On the inner region, the only cutoff error comes from the initial time transition.

theorem ESS.ucGaussianCutoff_field_eq_on_inner_late {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucInnerRegion ρ) (hlate : 2 * ε < z.2) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v z = v z

The compact field equals the original field on the late interior.

theorem ESS.ucGaussianCutoff_dw_eq_on_inner_late {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucInnerRegion ρ) (hlate : 2 * ε < z.2) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) : ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv z = Dv z

The first weak derivative data agree on the late interior.

theorem ESS.ucInitialTimeCutoff_deriv_zero_below {ε s : ℝ} (hε : 0 < ε) (hs : s < ε) : deriv (ucInitialTimeCutoff ε) s = 0

The initial cutoff derivative vanishes before its transition.

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

The initial cutoff derivative is confined to the early time interval.