OAI/NumberTheory/Ostmann/ZeroDensity/PrimePowerRemainder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform control of the prime-power remainder in the Euler identity

  1. def OAI.Ostmann.primePowerRemainder line 12
  2. theorem OAI.Ostmann.primePowerRemainder_summable_one line 15
  3. theorem OAI.Ostmann.primePowerRemainder_twist_norm_le line 31
  4. theorem OAI.Ostmann.exists_primePowerRemainder_bound line 42

    Source documentation

    A single absolute constant bounds all higher-prime-power contributions, uniformly in the modulus, character and real s >= 1.

    theorem exists_primePowerRemainder_bound :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (q : ℕ) (χ : DirichletCharacter ℂ q) (s : ℝ), 1 ≤ s →
      LSeriesSummable (fun n => χ n * primePowerRemainder n) (s : ℂ) ∧
        ‖LSeries (fun n => χ n * primePowerRemainder n) (s : ℂ)‖ ≤ C := by
…

    Mentions: OAI.Ostmann.primePowerRemainder