Weighted collar error

The heat cutoff error on the spatial and final time collar is controlled by the unweighted field energy with Gaussian exponential decay.

theorem ESS.uc_gaussian_collar_error_sq_le {ρ c₁ scale : ℝ} (hρ : 4 ≤ ρ) (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) : have a := 1 / 100 * ρ ^ 2 / (2 * Real.log (CKN.gaussCarlemanTimeWeight (3 / 2))); have A := 32 + 3 * (CKN.cutoffSecondDerivativeConstant / ρ ^ 2) + 3 * c₁ * scale * (CKN.cutoffGradientConstant / ρ); have B := 18 * (CKN.cutoffGradientConstant / ρ); ucGaussianWeight a z * (3 * (if z ∈ ucCutoffRegion ρ then A * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + B * √(CKN.spatialGradientSq v Dv z) else 0) ^ 2) ≤ 6 * Real.exp (-ρ ^ 2 / 100) * (A ^ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + B ^ 2 * CKN.spatialGradientSq v Dv z)

The squared collar error is bounded by the full energy multiplied by the Gaussian collar exponential.

theorem ESS.uc_gaussian_collar_error_integral_le {ρ c₁ scale : ℝ} (hρ : 4 ≤ ρ) {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 < ⊤) : have a := 1 / 100 * ρ ^ 2 / (2 * Real.log (CKN.gaussCarlemanTimeWeight (3 / 2))); have A := 32 + 3 * (CKN.cutoffSecondDerivativeConstant / ρ ^ 2) + 3 * c₁ * scale * (CKN.cutoffGradientConstant / ρ); have B := 18 * (CKN.cutoffGradientConstant / ρ); MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ucGaussianWeight a z * (3 * (if z ∈ ucCutoffRegion ρ then A * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + B * √(CKN.spatialGradientSq v Dv z) else 0) ^ 2)) (ucCylinder ρ) MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ucGaussianWeight a z * (3 * (if z ∈ ucCutoffRegion ρ then A * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + B * √(CKN.spatialGradientSq v Dv z) else 0) ^ 2) ≤ 6 * Real.exp (-ρ ^ 2 / 100) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, A ^ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + B ^ 2 * CKN.spatialGradientSq v Dv z

The total weighted collar error is bounded by exponentially damped unweighted field and gradient energy.