OAI/NumberTheory/JointDickman/Probability/GraphResidueNormalization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.graph_selected_odds_bound line 12
2. theorem OAI.JointDickman.three_root_product_le_half_cube line 44
3. theorem OAI.JointDickman.primeNormalizer_sdiff line 64
4. theorem OAI.JointDickman.graph_three_root_normalization line 78

   Source documentation

   This is uniform in the later regularity cutoff. Only Mertens' cited reciprocal-prime input is used for the normalization.

   theorem graph_three_root_normalization
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
         ∀ S : Finset ℕ, S ⊆ auxiliaryPrimes B →
         (∏ p ∈ S, p : ℕ) ≤ Real.exp (10*(B : ℝ)) →
         (auxiliaryRatio B^(1/2 : ℝ))^3 *
           (∏ p ∈ auxiliaryPrimes B\S, (1-3/(2*(p : ℝ)))) ≤ K := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryRatio