OneSidedDecayBudget.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The separated long/short scales absorb the one-sided losses

theorem OAI.Ostmann.eventual_polynomial_log_budget line 11

theorem OAI.Ostmann.eventual_separated_character_error line 31

Source documentation

The square-mean off-diagonal error after all polynomial history costs. The long logarithmic scale β exceeds both the short scale γ and the desired error scale α.

theorem eventual_separated_character_error (C z α β γ c : ℝ) (d : ℕ)
    (hC : 0 ≤ C) (hz : 0 ≤ z) (hα : 0 < α) (hαβ : α < β)
    (hγβ : γ < β) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ m : ℝ, 0 ≤ m → m ≤ z * L →
      Real.exp (C * (1 + m) ^ d + 2 * Real.exp (γ * L) - Real.exp (β * L)) ≤
        Real.exp (-c * Real.exp (α * L)) := by
…

theorem OAI.Ostmann.eventual_diagonal_atom_error line 57

Source documentation

The small diagonal atom remains exponentially small after multiplication by every fixed polynomial-in-m exponential loss.

theorem eventual_diagonal_atom_error (C z α c : ℝ) (d : ℕ)
    (hC : 0 ≤ C) (hz : 0 ≤ z) (hα : 0 < α) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ m : ℝ, 0 ≤ m → m ≤ z * L →
      2 * Real.exp (C * (1 + m) ^ d - c * Real.exp (α * L)) ≤
        Real.exp (-(c / 2) * Real.exp (α * L)) := by
…

theorem OAI.Ostmann.norm_le_exp_half_of_sq_le line 76

theorem OAI.Ostmann.eventual_one_sided_squared_budget line 86

Source documentation

Both parts of the expanded square, including all fixed polynomial losses, obey one common smallness bound.

theorem eventual_one_sided_squared_budget (C z α β γ c : ℝ) (d : ℕ)
    (hC : 0 ≤ C) (hz : 0 ≤ z) (hα : 0 < α) (hαβ : α < β)
    (hγβ : γ < β) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ m : ℝ, 0 ≤ m → m ≤ z * L →
      Real.exp (C * (1 + m) ^ d) *
        (Real.exp (-c * Real.exp (α * L)) +
          Real.exp (2 * Real.exp (γ * L) - Real.exp (β * L))) ≤
        Real.exp (-(c / 2) * Real.exp (α * L)) := by
…

theorem OAI.Ostmann.eventual_one_sided_amplitude_budget line 109