OAI/NumberTheory/Ostmann/Characters/CharacterResolventBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform control of differences of zero resolvents

  1. theorem OAI.Ostmann.ratio_triangle_bound line 12
  2. theorem OAI.Ostmann.zero_resolvent_difference_bound line 30

    Source documentation

    An inverse difference is controlled by the positive real zero kernel at its reference point. This makes the bound summable over actual zeros.

    theorem zero_resolvent_difference_bound (s w ρ : ℂ) (A δ : ℝ)
    (hA : 0 ≤ A) (hδ : 0 < δ) (hsep : δ ≤ ‖s - ρ‖)
    (hshift : ‖w - s‖ ≤ A) (hre : 1 ≤ (w - ρ).re) :
    ‖(s - ρ)⁻¹ - (w - ρ)⁻¹‖ ≤
      A * (1 + A / δ) * ((w - ρ)⁻¹).re := by
…