OAI/NumberTheory/JointDickman/Arithmetic/SquarefreeLogarithmicIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic prime decomposition for squarefree-supported coefficients

This is the coefficient identity used to start the Montgomery--Vaughan bilinear reduction. The error is supported on prime-square divisibility.

  1. lemma OAI.JointDickman.squarefree_log_eq_sum_primeFactors line 13
  2. lemma OAI.JointDickman.multiplicative_squarefree_log_identity line 21
  3. lemma OAI.JointDickman.squarefree_supported_log_error line 34

    Source documentation

    Prime powers cause the only error when the logarithmic identity is used without restricting the outer sum to squarefree integers.

    lemma squarefree_supported_log_error (f : ArithmeticFunction ℝ)
    (hf : f.IsMultiplicative) (hb : ∀ n, |f n| ≤ 1)
    (hsupport : ∀ n, ¬Squarefree n → f n = 0) (n : ℕ) :
    |f n*Real.log n - ∑ p ∈ n.primeFactors, (f p*f (n/p))*Real.log p| ≤
      ∑ p ∈ n.primeFactors, if p^2 ∣ n then Real.log p else 0 := by
…