Parameters for Gaussian average decay

The Carleman absorption choice and the rescaled collar geometry in lem:bu-gaussian.

theorem ESS.buGaussian_parameter_choice (c₁ C_G β H : ℝ) (hc₁ : 0 < c₁) (hCG : 0 < C_G) (hβ : 0 < β) (hH : 0 < H) : ∃ (γ : ℝ), 0 < γ ∧ γ < 1 / 12 ∧ γ ≤ 1 / 24 ∧ γ ≤ β / (3 * H) ∧ 3 * C_G * c₁ ^ 2 * γ ≤ 1 / 2

A small time threshold satisfying the absorption conditions in lem:bu-gaussian#parameter-choice.

theorem ESS.buGaussian_parameter_geometry (β H γ x₃ t : ℝ) (hβ : 0 < β) (hH : 0 < H) (hHβ : 16 * β < H) (hγβ : γ ≤ β / (3 * H)) (hx₃ : 2 < x₃) (ht : 0 < t) (htγ : t < γ) : have ρ := (x₃ - 1) / √(3 * t); have a := β * ρ ^ 2 / H; have r := 1 / (16 * √a); 4 < ρ ∧ 1 < a ∧ 0 < r ∧ r < 1 / 16 ∧ ρ * r = √(H / β) / 16

The source parameter choice makes the rescaled shell radius large, the Carleman exponent greater than one, and the covering radius at most 1/16. The product rho times r is independent of the point and time.

theorem ESS.buGaussian_scaled_height_lower {x₃ t : ℝ} (hx₃ : 2 < x₃) (ht : 0 < t) : ((x₃ - 1) / √(3 * t)) ^ 2 ≥ x₃ ^ 2 / (12 * t)

The rescaled collar radius gives the source height-decay exponent (lem:bu-gaussian#change-back).