Energy Bootstrap

theorem EulerEnergyBootstrap.radius_bounds (C B Δ ρ₀ S R₀ : ℝ) (hC : 0 ≤ C) (hB : 0 ≤ B) (hΔ : 0 ≤ Δ) (hρ : 0 < ρ₀) (_hS : 0 ≤ S) (hR : 0 ≤ R₀) (hdecay : 2 * C * (B + Δ) * S ≤ ρ₀ / 2) (hscale : ρ₀ * R₀ ≤ 1) (t : ℝ) (ht : t ∈ Set.Icc 0 S) : ρ₀ / 2 ≤ ρ₀ - 2 * C * (B + Δ) * t ∧ 0 < ρ₀ - 2 * C * (B + Δ) * t ∧ (ρ₀ - 2 * C * (B + Δ) * t) * R₀ ≤ 1

theorem EulerEnergyBootstrap.shrinking_radius_cancels_loss (C B Δ ρ R₀ X : ℝ) (hC : 0 ≤ C) (hB : 0 ≤ B) (hΔ : 0 ≤ Δ) (hρ : 0 < ρ) (hR : 0 ≤ R₀) (hscale : ρ * R₀ ≤ 1) (hX : X ≤ Δ) : -2 * C * (B + Δ) / ρ + C * (ρ⁻¹ + R₀) * (B + X) ≤ 0

theorem EulerEnergyBootstrap.close_energy_estimate (X X' Y : ℝ → ℝ) (C B Δ r ρ₀ S R₀ : ℝ) (hC : 0 < C) (hB : 0 ≤ B) (hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1) (hr : 0 < r) (hρ : 0 < ρ₀) (hS : 0 ≤ S) (hR : 0 ≤ R₀) (hdecay : 2 * C * (B + Δ) * S ≤ ρ₀ / 2) (hscale : ρ₀ * R₀ ≤ 1) (hsmall : 2 * r * Real.exp (3 * C * S) ≤ Δ / 2) (hcont : ContinuousOn X (Set.Icc 0 S)) (hinit : X 0 ≤ 2 * r) (hder : ∀ t ∈ Set.Ico 0 S, HasDerivAt X (X' t) t) (hY : ∀ t ∈ Set.Ico 0 S, 0 ≤ Y t) (hineq : ∀ t ∈ Set.Ico 0 S, X' t ≤ C * (X t + X t ^ 2 + r) + (-2 * C * (B + Δ) / (ρ₀ - 2 * C * (B + Δ) * t) + C * ((ρ₀ - 2 * C * (B + Δ) * t)⁻¹ + R₀) * (B + X t)) * Y t) (t : ℝ) : t ∈ Set.Icc 0 S → X t ≤ 2 * r * Real.exp (3 * C * t) ∧ X t ≤ Δ / 2

The shrinking-radius energy inequality closes without assuming the bootstrap conclusion.

theorem EulerEnergyBootstrap.quadratic_stability (X X' : ℝ → ℝ) (C ε S : ℝ) (hC : 0 < C) (hε : 0 < ε) (hS : 0 ≤ S) (hsmall : 2 * ε * Real.exp (3 * C * S) ≤ 1 / 2) (hcont : ContinuousOn X (Set.Icc 0 S)) (hinit : X 0 ≤ ε) (hder : ∀ t ∈ Set.Ico 0 S, HasDerivAt X (X' t) t) (hineq : ∀ t ∈ Set.Ico 0 S, X' t ≤ C * (X t + X t ^ 2)) (t : ℝ) : t ∈ Set.Icc 0 S → X t ≤ 2 * ε * Real.exp (3 * C * S)

Uniform stability from a quadratic differential inequality and small initial error.