OAI/NumberTheory/Ostmann/Construction/PrimeProductMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.inverse_choose_le line 13
2. theorem OAI.Ostmann.prime_product_mean_le_odd_sum line 32

   Source documentation

   Positivity transfers any statistic of the prime product to all odd moduli in its range; unique factorization gives the exact uniform weight.

   theorem prime_product_mean_le_odd_sum (P : Finset ℕ) (k Z : ℕ)
       (hP : ∀ p ∈ P, p.Prime) (hodd : ∀ p ∈ P, Odd p)
       (hZ : ∀ p ∈ P, p ≤ Z) (F : ℕ → ℝ) (hF : ∀ m, 0 ≤ F m) :
       (P.card.choose k : ℝ)⁻¹ * (∑ m ∈ primeSubsetProducts P k, F m) ≤
         (P.card.choose k : ℝ)⁻¹ *
           (∑ m ∈ Finset.range (Z ^ k + 1), if Odd m then F m else 0) := by
   …

   Mentions: OAI.Ostmann.primeSubsetProducts

3. theorem OAI.Ostmann.prime_product_family_moment_bound line 59

   Source documentation

   This is the finite, explicit version of the manuscript's uniform Jacobi-family moment estimate, before its final numerical specialization.

   theorem prime_product_family_moment_bound (hB : PublishedBonamiBound)
       {I : Type*} [Fintype I] (P S R : Finset ℕ)
       (hS : ∀ s ∈ S, Squarefree s) (hR : ∀ s ∈ S, s.primeFactors ⊆ R)
       (hP : ∀ p ∈ P, p.Prime) (hodd : ∀ p ∈ P, Odd p)
       (U Z k l : ℕ) (hU : ∀ s ∈ S, s ≤ U) (hZ : ∀ p ∈ P, p ≤ Z)
       (hl : 0 < l) (hk : 1 ≤ k) (hsize : 2 * k ^ 2 ≤ P.card)
       (b : I → S → ℂ) (pick : ℕ → I) (E A : ℝ)
       (henergy : ∀ i, (∑ s : S, ((2 * l - 1 : ℕ) : ℝ) ^ s.val.primeFactors.card * ‖b i s‖ ^ 2) ≤ E)
       (hmass : ∀ i, (∑ s : S, ‖b i s‖) ≤ A) :
       (P.card.choose k : ℝ)⁻¹ *
           (∑ m ∈ primeSubsetProducts P k,
             ‖∑ s : S, b (pick m) s * (realJacobi s.val m : ℂ)‖ ^ (2 * l)) ≤
   …

   Mentions: OAI.Ostmann.PublishedBonamiBound, OAI.Ostmann.primeSubsetProducts, OAI.Ostmann.realJacobi