Quantitative cutoff errors

The finite dimensional gradient estimates control the terms created by spatial differentiation of the Gaussian cutoff.

theorem ESS.uc_gradient_component_le (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) (i j : Fin 3) : |Dv z i j| ≤ √(CKN.spatialGradientSq v Dv z)

Each weak gradient component is bounded by the full Euclidean gradient magnitude.

theorem ESS.uc_gradient_contraction_le (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) (d : Fin 3 → ℝ) (M : ℝ) (hM : 0 ≤ M) (hd : ∀ (j : Fin 3), |d j| ≤ M) : (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => ∑ j : Fin 3, d j * Dv z i j) ≤ 9 * M * √(CKN.spatialGradientSq v Dv z)

A scalar coefficient bounded componentwise by M produces a controlled vector when contracted with the spatial gradient.

theorem ESS.ucGaussianCutoff_heat_error_le {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) (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) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.vec3EuclideanNorm (ucCutoffHeat (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv D2v Dtv z - ucGaussianCutoff ρ hρ ε z • ucWeakHeatVector D2v Dtv z) ≤ |CKN.timePartial (ucGaussianCutoff ρ hρ ε) z + ∑ j : Fin 3, CKN.spatialSecondPartial (ucGaussianCutoff ρ hρ ε) j j z| * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + 18 * (CKN.cutoffGradientConstant / ρ) * √(CKN.spatialGradientSq v Dv z)

The heat operator error caused by cutoff differentiation is bounded by the cutoff derivatives and the original field energy.

theorem ESS.ucGaussianCutoff_laplacian_abs_bound {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : |∑ j : Fin 3, CKN.spatialSecondPartial (ucGaussianCutoff ρ hρ ε) j j z| ≤ 3 * (CKN.cutoffSecondDerivativeConstant / ρ ^ 2)

The trace of the cutoff Hessian is bounded by the three diagonal second derivatives.

theorem ESS.ucGaussianCutoff_timePartial_local_bound {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucCylinder ρ) : |CKN.timePartial (ucGaussianCutoff ρ hρ ε) z| ≤ (if z ∈ ucCutoffRegion ρ then 32 else 0) + if ε ≤ z.2 ∧ z.2 ≤ 2 * ε then 8 / ε else 0

The cutoff time derivative splits into a collar contribution and an early-time contribution.

theorem ESS.ucGaussianCutoff_laplacian_abs_local_bound {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucCylinder ρ) : |∑ j : Fin 3, CKN.spatialSecondPartial (ucGaussianCutoff ρ hρ ε) j j z| ≤ if z ∈ ucCutoffRegion ρ then 3 * (CKN.cutoffSecondDerivativeConstant / ρ ^ 2) else 0

The cutoff Laplacian vanishes on the inner plateau and is bounded on its collar.

theorem ESS.ucGaussianCutoff_spatialPartial_abs_local_bound {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucCylinder ρ) (j : Fin 3) : |CKN.spatialPartial (ucGaussianCutoff ρ hρ ε) j z| ≤ if z ∈ ucCutoffRegion ρ then CKN.cutoffGradientConstant / ρ else 0

The spatial cutoff derivative vanishes off the collar inside the normalized cylinder.

theorem ESS.ucGaussianCutoff_heat_error_eq_on_inner {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucInnerRegion ρ) (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) : ucCutoffHeat (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv D2v Dtv z - ucGaussianCutoff ρ hρ ε z • ucWeakHeatVector D2v Dtv z = deriv (ucInitialTimeCutoff ε) z.2 • v z

The cutoff heat error on the inner region is exactly the derivative of the initial time factor times the original field.

theorem ESS.ucGaussianCutoff_heat_error_local_le {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (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) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucCylinder ρ) : CKN.Foundation.Parabolic.vec3EuclideanNorm (ucCutoffHeat (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv D2v Dtv z - ucGaussianCutoff ρ hρ ε z • ucWeakHeatVector D2v Dtv z) ≤ (if z ∈ ucCutoffRegion ρ then (32 + 3 * (CKN.cutoffSecondDerivativeConstant / ρ ^ 2)) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + 18 * (CKN.cutoffGradientConstant / ρ) * √(CKN.spatialGradientSq v Dv z) else 0) + (if ε ≤ z.2 ∧ z.2 ≤ 2 * ε then 8 / ε else 0) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)

The cutoff heat error is supported on the spatial or final-time collar and on the initial time transition.

theorem ESS.ucGaussianCutoff_heat_ae_local_bound {ρ ε c₁ scale : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (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) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (ucCylinder ρ), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z))) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (ucCylinder ρ), z ∈ ucCylinder ρ → CKN.Foundation.Parabolic.vec3EuclideanNorm (ucCutoffHeat (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv D2v Dtv z) ≤ (ucGaussianCutoff ρ hρ ε z * (c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z))) + if z ∈ ucCutoffRegion ρ then (32 + 3 * (CKN.cutoffSecondDerivativeConstant / ρ ^ 2)) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + 18 * (CKN.cutoffGradientConstant / ρ) * √(CKN.spatialGradientSq v Dv z) else 0) + (if ε ≤ z.2 ∧ z.2 ≤ 2 * ε then 8 / ε else 0) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)

The normalized differential inequality and the localized cutoff errors control the heat operator of the compact field.