OAI/NumberTheory/JointDickman/Amplification/NearCofactorMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.halasz_phase_factor_decay line 10
2. lemma OAI.JointDickman.halasz_phase_mean_norm line 20
3. theorem OAI.JointDickman.near_zero_masked_mean line 33

   Source documentation

   Near-twist renormalization gives reciprocal-frequency cancellation around zero, uniformly in the deleted small-prime set.

   theorem near_zero_masked_mean : ∃ C : ℝ, 0 < C ∧
       ∀ᶠ N : ℕ in atTop, ∀ F : ℕ → ℂ,
         F 1 = 1 → Multiplicative F → OneBounded F →
         ∀ Q : Finset ℕ, (∀ p ∈ Q, p.Prime) →
         (∀ p ∈ Q, (p:ℝ) ≤ Real.exp (Real.sqrt (Real.log N))) →
         squaredDistance F (mrtArchimedeanTwist 0) N ≤ Real.log (Real.log N)/8 →
         ∀ t : ℝ, |t| ≤ (Real.log N)^((1:ℝ)/16) →
         ‖halaszPhaseMean (mrtMissingCoefficient F Q) t N‖ ≤
           (2/(1+|t|)+C*(Real.log N)^(-(1:ℝ)/16))*N := by
   …

4. theorem OAI.JointDickman.near_zero_count_prefix line 72

   Source documentation

   The reciprocal prime-count denominator is handled by its exact integral of multiplicative soft masks, with no loss near frequency zero.

   theorem near_zero_count_prefix : ∃ C : ℝ, 0 < C ∧
       ∀ᶠ N : ℕ in atTop, ∀ F : ℕ → ℂ,
         F 1 = 1 → Multiplicative F → OneBounded F →
         ∀ Q P : Finset ℕ, (∀ p ∈ Q, p.Prime) → (∀ p ∈ P, p.Prime) →
         (∀ p ∈ Q, (p:ℝ) ≤ Real.exp (Real.sqrt (Real.log N))) →
         squaredDistance F (mrtArchimedeanTwist 0) N +
           (∑ p ∈ P, 1/(p:ℝ)) ≤ Real.log (Real.log N)/8 →
         ∀ t : ℝ, |t| ≤ (Real.log N)^((1:ℝ)/16) →
         ‖∑ n ∈ Icc 1 N,
           (mrtMissingCoefficient F Q n * conj (mrtArchimedeanTwist t n))/
             ((finitePrimeDivisorCount P n:ℂ)+1)‖ ≤
           (2/(1+|t|)+C*(Real.log N)^(-(1:ℝ)/16))*N := by
   …