UniformPrimeProductMoment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-family moment bound under the original prime-product law

theorem OAI.Ostmann.eventual_uniform_prime_product_moment line 15

Source documentation

The manuscript's fixed-family estimate. All sampling and numerical transfer factors are discharged; only Bonami's precisely stated published inequality is an analytic input to this moment calculation.

theorem eventual_uniform_prime_product_moment (hB : PublishedBonamiBound)
    (C ε : ℝ) (hC : 1 ≤ C) (hε : 0 < ε) :
    ∀ᶠ T : ℝ in atTop, ∀ {I : Type*} [Fintype I]
      (P S R : Finset ℕ) (U Z k l : ℕ),
      (∀ s ∈ S, Squarefree s) → (∀ s ∈ S, s.primeFactors ⊆ R) →
      (∀ p ∈ P, p.Prime) → (∀ p ∈ P, Odd p) →
      (∀ s ∈ S, s ≤ U) → (∀ p ∈ P, p ≤ Z) →
      1 ≤ Z → Real.exp T ≤ C * T * P.card → (Z : ℝ) ≤ Real.exp (T + 1) →
      1 ≤ k → 2 * k ^ 2 ≤ P.card →
      T ^ (3 / 5 : ℝ) / 2 ≤ k → (k : ℝ) ≤ 2 * T ^ (3 / 5 : ℝ) →
      1 ≤ l → T ^ (1 / 1000000 : ℝ) / 2 ≤ l → (l : ℝ) ≤ T ^ (1 / 1000000 : ℝ) →
      (Fintype.card I : ℝ) ≤ Real.exp (C * T) → (U : ℝ) ≤ Real.exp (C * T) →
…

Mentions: OAI.Ostmann.PublishedBonamiBound