OAI/NumberTheory/JointDickman/Arithmetic/RoughPhaseEstimate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.power_lower_subset_card line 9
2. theorem OAI.JointDickman.rough_phase_mean_bound line 26

   Source documentation

   The remaining error is the near-cutoff prime-product mass plus the explicit repeated-prime exception. All estimates here are unconditional.

   theorem rough_phase_mean_bound : ∃ C : ℝ, 0 ≤ C ∧
       ∀ (P : Finset ℕ) (F : ℕ → ℂ) (t y Y : ℝ) (N J K : ℕ),
         0 < N → K ≠ 0 → 2 ≤ y → 1 ≤ Y → Y ≤ N →
         (∀ p ∈ P, p.Prime ∧ y < (p:ℝ) ∧ K < p) →
         F 1 = 1 → Multiplicative F → OneBounded F →
         (∀ p k : ℕ, p.Prime → p ∉ P → p^k ≤ N → F (p^k) = 1) →
         (∀ D ∈ P.powerset, (∏ p ∈ D, (p:ℝ)) ≤ N → D.card ≤ J) →
         ‖halaszPhaseMean F t N‖/(N:ℝ) ≤
           (2/(1+|t|)+9*(1+|t|)*Y/N)*Real.exp (2*∑ p ∈ P, 1/(p:ℝ))+
           2^J*((Real.log ((N:ℝ)/Y)+C)/Real.log y)*
             (∑ h ∈ range J, (∑ p ∈ P, 1/(p:ℝ))^h)+2/(K:ℝ) := by
   …