CharacterRectangleLog.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Analytic logarithms on the character zero-free rectangles

def OAI.JointDickman.characterContourWidth line 10
theorem OAI.JointDickman.exists_analytic_log_with_value line 13

theorem OAI.JointDickman.character_rectangle_log line 27

Source documentation

A normalized logarithm exists uniformly on rectangles with a power-sized width.

theorem character_rectangle_log {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) :
    ∃ A : ℝ, 0 < A ∧ A ≤ 1/4 ∧
      ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q), χ ≠ 1 →
      ∀ T : ℝ, 0 < T → ∀ v : ℂ, Complex.exp v = χ.LFunction (3/2) →
      ∃ f : ℂ → ℂ,
        AnalyticOnNhd ℂ f (zetaOpenRectangle (characterContourWidth A ε q T) T) ∧
        f (3/2) = v ∧ ∀ s ∈ zetaOpenRectangle (characterContourWidth A ε q T) T,
          Complex.exp (f s) = χ.LFunction s := by
…

Mentions: OAI.JointDickman.zetaOpenRectangle, OAI.JointDickman.characterContourWidth