Algebra of the Gaussian cutoff errors #
The four cutoff errors reduce to a cubic Gaussian tail after the main
Carleman term is absorbed (eq:bu-gaussian-collar).
theorem
ESS.buGaussian_error_assembly_bound
{c₀ k₀ k₁ Cacc a ρ T I E shell0 shell1 SM SG LM IM R F ε : ℝ}
(hc₀ : 0 ≤ c₀)
(hk₀ : 0 ≤ k₀)
(hk₁ : 0 ≤ k₁)
(hCacc : 0 ≤ Cacc)
(ha : 0 ≤ a)
(hρ : 0 ≤ ρ)
(hT : 0 ≤ T)
(hI : I ≤ 2 * c₀ * E)
(hE : E = 8 * shell0 ^ 2 * SM + 8 * shell1 ^ 2 * SG + 4096 * LM + 256 / ε ^ 2 * IM)
(hshell0 : 0 ≤ shell0)
(hshell0le : shell0 ≤ k₀)
(hshell1 : 0 ≤ shell1)
(hshell1le : shell1 ≤ k₁)
(hSM0 : 0 ≤ SM)
(hSG0 : 0 ≤ SG)
(hSM : SM ≤ 24 * ρ ^ 3 * T)
(hSG : SG ≤ F * R)
(hF : F ≤ Cacc * (1 + a))
(hR0 : 0 ≤ R)
(hR : R ≤ 24 * ρ ^ 3 * T)
(hLM : LM ≤ 12 * ρ ^ 3 * T)
(hIM : 256 / ε ^ 2 * IM ≤ T)
:
The shell, late-time, and initial-time estimates imply a uniform polynomial multiple of the radial Gaussian tail.
theorem
ESS.buGaussian_final_scalar_bound
{β H c P Ctail Ccore E T ρ a x₃ t D I : ℝ}
(hβ : 0 < β)
(hH : 0 < H)
(hρone : 1 ≤ ρ)
(ha : a = β / H * ρ ^ 2)
(hT : T = E * Real.exp (-2 * β * ρ ^ 2))
(hCtail : Ctail = 64 * (1 + β / (2 * H)) / (β / 2) ^ 2 / √β)
(hCcore : Ccore = 2 * Real.exp (3 / 2) * c * P * Ctail)
(hHeight : x₃ ^ 2 / (12 * t) ≤ ρ ^ 2)
(hMass : Real.exp (-(3 / 2)) * D ≤ I)
(hI : I ≤ 2 * c * P * ((1 + a) * (1 + ρ) ^ 3 * T))
(hc : 0 ≤ c)
(hP : 0 ≤ P)
(hE : 0 ≤ E)
:
The polynomial collar loss is absorbed into the radial exponential, and the scaled distance yields the physical height decay.