Removing the two compact cutoff parameters

The lower-time transition is removed first at fixed spatial radius; the spatial shell is removed second.

theorem ESS.bu_short_two_parameter_limit (L A : ℝ) (shell : ℕ → ℝ) (early : ℕ → ℝ → ℝ) (n₀ : ℕ) (ε₀ : ℝ) (hε₀ : 0 < ε₀) (hshell : Filter.Tendsto shell Filter.atTop (nhds 0)) (hearly : ∀ (n : ℕ), Filter.Tendsto (early n) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (hbound : ∀ (n : ℕ), n₀ ≤ n → ∀ (ε : ℝ), 0 < ε → ε < ε₀ → L ≤ A + shell n + early n ε) : L ≤ A

Successive vanishing of a lower-time error and a spatial shell error leaves the fixed phase-gap bound.

theorem ESS.bu_short_eq_zero_of_exponential_bound {I C D a₀ : ℝ} (hI : 0 ≤ I) (hD : 0 < D) (hbound : ∀ (a : ℝ), a₀ < a → I ≤ C * Real.exp (-(a * D))) : I = 0

A nonnegative quantity bounded by a decaying exponential at every large parameter must vanish.