WeightedProgressionRates.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Numerical error budgets for the weighted giant comparison

theorem OAI.Ostmann.PublishedProgressionInput.log_interval_budget_rate line 13

Source documentation

The explicit published-input error bound itself has the required uniform rate, before a continuous weight or residue-cell count is inserted.

theorem PublishedProgressionInput.log_interval_budget_rate (P : PublishedProgressionInput)
    (a₀ μ δ : ℝ) (hδa : δ < a₀ / 2) (hδμ : δ < a₀ - μ)
    (ha : 0 < a₀) (haμ : 0 < a₀ - μ) :
    ∀ᶠ L : ℝ in atTop, ∀ Q : ℕ, 2 ≤ Q →
      Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp (μ * L) →
      ∀ u : ℝ, Real.exp (a₀ * L) ≤ u →
      18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt u) +
        Real.exp (-P.kappa * u / Real.log (4 * (Q : ℝ))) ≤
          2 * Real.exp (-Real.exp (δ * L)) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput

theorem OAI.Ostmann.PublishedProgressionInput.weighted_giant_budget_rate line 49

Source documentation

The giant row of Section 8.2 absorbs all fixed-depth variation, normalization and residue-count costs. The threshold precedes every modulus, endpoint and weight budget.

theorem PublishedProgressionInput.weighted_giant_budget_rate (P : PublishedProgressionInput)
    (C : ℝ) (d : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ Q : ℕ, 2 ≤ Q →
      Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp ((12 / 1000 : ℝ) * L) →
      ∀ u V : ℝ, Real.exp ((49 / 1000 : ℝ) * L) ≤ u →
      V ≤ Real.exp (C * L ^ d + C * L * Real.exp ((12 / 1000 : ℝ) * L)) →
      V * (18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt u) +
        Real.exp (-P.kappa * u / Real.log (4 * (Q : ℝ)))) ≤
          Real.exp (-Real.exp ((13 / 1000 : ℝ) * L)) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput