Uniform collar coefficient

The spatial covering radius is inverse to the square root of the Gaussian parameter. This keeps every weight comparison factor independent of the rescaling point in eq:bu-gaussian-collar.

theorem ESS.buGaussian_shell_coefficient_bound {a r ρ scale c₁ R₀ : ℝ} (ha : 0 < a) (hr : r = 1 / (16 * √a)) (hR : ρ * r = R₀) (hscale : scale ^ 2 ≤ 1 / 4) : Real.exp (2 * (56 * a * (2 * r) ^ 2 + 12 * ρ * (2 * r) + 36 * ρ ^ 2 * (2 * r) ^ 2)) * (256 * (1 + (c₁ * scale) ^ 2 + 1 / (2 * r / 2) ^ 2)) * (8 * ↑(Besicovitch.multiplicity CKN.BUGaussianSpace) ^ 2) ≤ Real.exp (2 * (56 / 64 + 24 * R₀ + 144 * R₀ ^ 2)) * (256 * 256 * (1 + c₁ ^ 2)) * (8 * ↑(Besicovitch.multiplicity CKN.BUGaussianSpace) ^ 2) * (1 + a)

The weighted collar Caccioppoli coefficient grows at most linearly in its Gaussian parameter once the covering radius is fixed.

theorem ESS.buGaussian_shell_amplitude_bound {ρ scale c₁ Cg Cs : ℝ} (hρ : 4 < ρ) (hscale : 0 ≤ scale) (hscaleSq : scale ^ 2 ≤ 1 / 4) (hc₁ : 0 ≤ c₁) (hCg : 0 ≤ Cg) (hCs : 0 ≤ Cs) : 0 ≤ 32 + 3 * (Cs / ρ ^ 2) + 3 * c₁ * scale * (Cg / ρ) ∧ 32 + 3 * (Cs / ρ ^ 2) + 3 * c₁ * scale * (Cg / ρ) ≤ 32 + 3 * Cs + 3 * c₁ * Cg ∧ 0 ≤ 18 * (Cg / ρ) ∧ 18 * (Cg / ρ) ≤ 18 * Cg

The spatial cutoff coefficients are controlled by fixed derivative bounds once the localization radius exceeds four.

theorem ESS.buGaussian_shell_gradient_integral_bound {I R F C a M : ℝ} (hI : I ≤ F * R) (hF : F ≤ C * (1 + a)) (hR0 : 0 ≤ R) (hR : R ≤ M) (hC : 0 ≤ C * (1 + a)) : I ≤ C * (1 + a) * M

Apply the uniform collar coefficient to a nonnegative radial mass.

theorem ESS.buGaussian_polynomial_domination {a ρ : ℝ} (ha : 0 ≤ a) (hρ : 0 ≤ ρ) : 1 ≤ (1 + a) * (1 + ρ) ^ 3 ∧ ρ ^ 3 ≤ (1 + a) * (1 + ρ) ^ 3 ∧ (1 + a) * ρ ^ 3 ≤ (1 + a) * (1 + ρ) ^ 3

The fixed cubic polynomial dominates the volume factors in the Gaussian collar and late-time estimates.