OAI/NumberTheory/JointDickman/Amplification/FiniteWeightPhase.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.finitePrimeDivisorCount_mul_invariant line 11
2. theorem OAI.JointDickman.finite_weight_count_phase_expansion line 21

   Source documentation

   No limiting estimate is used: the fixed weight becomes finitely many rescaled prefix sums, with the original prime-count denominator retained.

   theorem finite_weight_count_phase_expansion (E P : Finset ℕ)
       (hE : ∀ p ∈ E, p.Prime) (hP : ∀ p ∈ P, p.Prime)
       (hdis : Disjoint E P) (w : ℕ → ℝ) (F : ℕ → ℂ)
       (hF : ∀ D ∈ E.powerset, ∀ n : ℕ, 0 < n →
         F ((∏ p ∈ D, p)*n) = F n) (t : ℝ) (N : ℕ) :
       (∑ n ∈ Icc 1 N, (F n*(finitePrimeWeight E w n:ℂ)*halaszPowerPhase t n)/
         ((finitePrimeDivisorCount P n:ℂ)+1)) =
       ∑ D ∈ E.powerset, ((∏ p ∈ D, (w p-1):ℝ):ℂ)*
         halaszPowerPhase t (∏ p ∈ D, (p:ℝ))*
         ∑ n ∈ Icc 1 (N/(∏ p ∈ D, p)),
           (F n*halaszPowerPhase t n)/((finitePrimeDivisorCount P n:ℂ)+1) := by
   …

   Mentions: OAI.JointDickman.finitePrimeWeight