RoughPrimePresence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Passing from ordinary multiplicative weights to prime presence

lemma OAI.JointDickman.primePresence_norm_le_one line 10

theorem OAI.JointDickman.rough_eq_primePresence line 21

Source documentation

Away from repeated active primes, prime-power agreement outside the active set identifies the ordinary multiplicative weight exactly.

theorem rough_eq_primePresence (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (F : ℕ → ℂ) (hF1 : F 1 = 1) (hFm : Multiplicative F)
    {N n : ℕ} (hn : 0 < n) (hnN : n ≤ N)
    (hlocal : ∀ p k : ℕ, p.Prime → p ∉ P → p^k ≤ N → F (p^k) = 1)
    (hsq : ∀ p ∈ P, ¬p^2 ∣ n) : F n = primePresence P F n := by
…

Mentions: OAI.JointDickman.primePresence

theorem OAI.JointDickman.rough_primePresence_phase_error line 46