OAI/NumberTheory/Ostmann/Construction/PrimeProductParameterBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventual_prime_product_parameter_budget line 13

   Source documentation

   The transfer-factor logarithm is negligible after division by the moment order. The small positive gap mu + kappa - 1 is used explicitly.

   theorem eventual_prime_product_parameter_budget (C ε : ℝ)
       (hC : 0 ≤ C) (hε : 0 < ε) :
       ∀ᶠ T : ℝ in atTop, ∀ k l : ℝ,
         0 ≤ k → k ≤ 2 * T ^ (3 / 5 : ℝ) →
         T ^ (1 / 1000000 : ℝ) / 2 ≤ l → l ≤ T ^ (1 / 1000000 : ℝ) →
         C * T + k * (C + 3 * Real.log T) + C * l ≤
           ε * l * T ^ (9999999 / 10000000 : ℝ) := by
   …

2. theorem OAI.Ostmann.eventual_prime_product_error_budget line 77

   Source documentation

   The nonsquare character-sum error is exponentially small because the number of sampled primes grows faster than the moment order.

   theorem eventual_prime_product_error_budget (C : ℝ) (hC : 0 ≤ C) :
       ∀ᶠ T : ℝ in atTop, ∀ k l : ℝ,
         T ^ (3 / 5 : ℝ) / 2 ≤ k →
         1 ≤ l → l ≤ T ^ (1 / 1000000 : ℝ) →
         C * T + C * l + 2 * C * l * T + k * (C + 3 * Real.log T - T) ≤
           -20 * l * T := by
   …