OAI/NumberTheory/JointDickman/Arithmetic/PrimeSquareErrorEstimate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The linear prime-square error in the logarithmic reduction

  1. lemma OAI.JointDickman.summable_log_div_square line 10
  2. lemma OAI.JointDickman.primeSquareLogError_eq line 29
  3. theorem OAI.JointDickman.primeSquareLogError_linear_bound line 63
  4. theorem OAI.JointDickman.squarefree_sum_prime_bilinear_bound line 87

    Source documentation

    The logarithmic prime-bilinear reduction with its O(N) error discharged.

    theorem squarefree_sum_prime_bilinear_bound : ∃ C : ℝ, 0 < C ∧
    ∀ (f : ArithmeticFunction ℝ), f.IsMultiplicative → (∀ n, |f n| ≤ 1) →
    (∀ n, ¬Squarefree n → f n = 0) → ∀ N : ℕ, 0 < N → ∀ θ : ℝ,
    Real.log N * ‖∑ n ∈ Ioc 0 N, (f n:ℂ)*additivePhase ((n:ℝ)*θ)‖ ≤
      C*N + ‖primeLogBilinear f N θ‖ := by
…

    Mentions: OAI.JointDickman.additivePhase, OAI.JointDickman.primeLogBilinear