OAI/NumberTheory/JointDickman/Arithmetic/RoughMiddleFrequency.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.rough_middle_frequency line 13

   Source documentation

   The prime-power support is literal: below the cutoff the function is one outside primes exceeding N^c. This covers the auxiliary count masks. No uniform short-interval theorem is used.

   theorem rough_middle_frequency {c : ℝ} (hc : 0 < c) (hc1 : c ≤ 1)
       {ε : ℝ} (hε : 0 < ε) :
       ∀ᶠ N : ℕ in atTop, ∀ (P : Finset ℕ) (F : ℕ → ℂ),
         (∀ p ∈ P, p.Prime ∧ (N:ℝ)^c < (p:ℝ) ∧ (p:ℝ) ≤ N) →
         F 1 = 1 → Multiplicative F → OneBounded F →
         (∀ p k : ℕ, p.Prime → p ∉ P → p^k ≤ N → F (p^k) = 1) →
         ∀ t : ℝ, (Real.log N)^((1:ℝ)/16) ≤ |t| → |t| ≤ 4*(Real.log N)^8 →
         ‖halaszPhaseMean F t N‖/(N:ℝ) ≤ ε := by
   …

2. theorem OAI.JointDickman.rough_middle_frequency_small_primes line 87

   Source documentation

   The application can specify the small-prime powers directly, without choosing a finite support set.

   theorem rough_middle_frequency_small_primes {c : ℝ} (hc : 0 < c) (hc1 : c ≤ 1)
       {ε : ℝ} (hε : 0 < ε) :
       ∀ᶠ N : ℕ in atTop, ∀ F : ℕ → ℂ,
         F 1 = 1 → Multiplicative F → OneBounded F →
         (∀ p k : ℕ, p.Prime → (p:ℝ) ≤ (N:ℝ)^c → p^k ≤ N → F (p^k) = 1) →
         ∀ t : ℝ, (Real.log N)^((1:ℝ)/16) ≤ |t| → |t| ≤ 4*(Real.log N)^8 →
         ‖halaszPhaseMean F t N‖/(N:ℝ) ≤ ε := by
   …