MovingPatternPrimeNormBudget.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Joining the giant error to the sharp original arithmetic budget

theorem OAI.Ostmann.movingPattern_original_prime_norm_budget line 13

Source documentation

The exact harmonic denominator can be discarded only after positivity. The giant comparison adds one error and leaves the sharp Fourier main term and its internal-class weight intact.

theorem movingPattern_original_prime_norm_budget (n : ℕ) (C : ℝ) (hC : 1 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (c : ℕ) (E U u r cost main bulk a : ℝ),
      c ≤ 4 * n * 2 ^ n → 1 ≤ E → E ≤ Real.exp (C * L) →
      0 ≤ U → U ≤ Real.exp (Real.exp ((12 / 1000 : ℝ) * L)) →
      1 ≤ u → 1 ≤ r → 0 ≤ cost → 0 ≤ main → 0 ≤ bulk →
      cost ≤ Real.exp (-Real.exp ((2 / 1000 : ℝ) * L)) →
      bulk ≤ Real.exp (-Real.exp ((125 / 100000 : ℝ) * L)) +
        2 * Real.exp (-Real.exp ((2 / 1000 : ℝ) * L)) →
      a ≤ ((2 : ℝ) ^ c * E ^ (4 * n * 2 ^ n - c) * U ^ c) *
          (Real.exp (-Real.exp ((125 / 10000 : ℝ) * L)) +
            Real.exp (-Real.exp ((1225 / 100000 : ℝ) * L))) +
        ((4 : ℝ) ^ c * E ^ (4 * n * 2 ^ n - c)) * (cost + main + bulk) / (u * r) →
…