Initial transition integral

The time indicator in the cutoff heat error is precisely integration over the initial transition interval.

theorem ESS.uc_initial_indicator_integral_eq {ρ ε a : ℝ} (hε : 0 < ε) (hε1 : ε < 1) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ucGaussianWeight a z * if ε ≤ z.2 ∧ z.2 ≤ 2 * ε then CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 else 0) = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Icc ε (2 * ε)), ucGaussianWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2

The indicator form of the early cutoff error equals the weighted integral over its time transition interval.

theorem ESS.uc_initial_indicator_error_tendsto_zero {ρ a : ℝ} (hρ : 4 ≤ ρ) (ha : 0 ≤ a) {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 2) v Dv D2v Dtv) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤) (hflat : UCIntegralFlatness 0 ρ 2 v) : Filter.Tendsto (fun (ε : ℝ) => 192 / ε ^ 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ucGaussianWeight a z * if ε ≤ z.2 ∧ z.2 ≤ 2 * ε then CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The initial cutoff error in the absorbed estimate vanishes as the cutoff reaches time zero.