RootCellErrorRates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The complete root-cell error retains a double-exponential saving

theorem OAI.Ostmann.weighted_giant_atom_rate line 13

theorem OAI.Ostmann.PublishedProgressionInput.root_cell_error_rate line 31

Source documentation

The number of root cells is fixed before X grows. This estimate includes both the weighted progression error and all retained endpoint-prime atoms.

theorem PublishedProgressionInput.root_cell_error_rate (P : PublishedProgressionInput)
    (C : ℝ) (d K : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ Q : ℕ, 2 ≤ Q →
      Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp ((12 / 1000 : ℝ) * L) →
      ∀ N : ℕ, N ≤ K → ∀ s V B : ℕ → ℝ,
      (∀ j < N, Real.exp ((49 / 1000 : ℝ) * L) ≤ s j) →
      (∀ j < N, V j ≤ Real.exp (C * L ^ d + C * L * Real.exp ((12 / 1000 : ℝ) * L))) →
      (∀ j < N, B j ≤ Real.exp (C * L ^ d + C * L * Real.exp ((12 / 1000 : ℝ) * L))) →
      (∑ j ∈ Finset.range N,
        (V j * (18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt (s j)) +
          Real.exp (-P.kappa * s j / Real.log (4 * (Q : ℝ)))) + B j * Real.exp (-(s j)))) ≤
        Real.exp (-Real.exp ((125 / 10000 : ℝ) * L)) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput

theorem OAI.Ostmann.PublishedProgressionInput.root_cell_prime_rate line 61

Source documentation

The complete smooth root-cell comparison, uniformly for every bounded multiplier and every polynomial family within the stated numerical budget.

theorem PublishedProgressionInput.root_cell_prime_rate (P : PublishedProgressionInput)
    (C : ℝ) (d K k : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ Q q a : ℕ, 2 ≤ Q → 1 ≤ q → q ≤ Q → a.Coprime q →
      Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp ((12 / 1000 : ℝ) * L) →
      ∀ u v : ℝ, Real.exp ((49 / 1000 : ℝ) * L) ≤ u → u ≤ v → v ≤ u + 1 →
      ∀ (F : Fin k → ClippedPolynomialFactor) (S : Finset ℝ), S.card + 1 ≤ K →
      (∀ i r, r ∈ (F i).polynomial.derivative.roots → r ∈ S) →
      ∀ (c : (S → Ordering) → ℂ) (B : ℝ), 0 ≤ B → (∀ code, ‖c code‖ ≤ B) →
      2 * B * smoothPolynomialBudget F ≤
        Real.exp (C * L ^ d + C * L * Real.exp ((12 / 1000 : ℝ) * L)) →
      ∃ (s : ℕ → ℝ) (N : ℕ) (b : ℕ → ℂ),
        Monotone s ∧ s 0 = u ∧ s N = v ∧ N ≤ S.card + 1 ∧ (∀ j, ‖b j‖ ≤ B) ∧
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.smoothPolynomialBudget