CharacterZeroFreeStrip.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A small zero-free strip for primitive nonprincipal characters

The width may be an arbitrary fixed negative power of the modulus and height. This is sufficient when both parameters are bounded by powers of a logarithm.

theorem OAI.JointDickman.half_plane_lipschitz line 13

theorem OAI.JointDickman.primitive_character_zero_free_strip line 28

Source documentation

A Siegel-type strip, with an ineffective constant but uniform modulus and height.

theorem primitive_character_zero_free_strip {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) :
    ∃ A : ℝ, 0 < A ∧ A ≤ 1/4 ∧
      ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q),
        χ.IsPrimitive → χ ≠ 1 → ∀ σ t : ℝ,
          1 - A * (((q:ℝ)+2)*(|t|+2))^(-ε) ≤ σ → σ ≤ 2 →
          A * (((q:ℝ)+2)*(|t|+2))^(-ε) ≤ ‖χ.LFunction (σ + I*t)‖ := by
…

theorem OAI.JointDickman.nonprincipal_character_zero_free_strip line 130

Source documentation

The same strip is zero-free for imprimitive nonprincipal characters.

theorem nonprincipal_character_zero_free_strip {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) :
    ∃ A : ℝ, 0 < A ∧ A ≤ 1/4 ∧
      ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q), χ ≠ 1 → ∀ σ t : ℝ,
        1 - A * (((q:ℝ)+2)*(|t|+2))^(-ε) ≤ σ → σ ≤ 2 →
        χ.LFunction (σ + I*t) ≠ 0 := by
…