OAI/NumberTheory/DukePrimeDegree/Arithmetic/NumberFieldResidue.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The regularized Dedekind zeta function

The analytic class number formula gives a positive residue and the one-sided limit of the regularized Dedekind zeta function at its pole.

  1. def OAI.DukePrimeDegree.regularizedZeta line 22

    Source documentation

    The real regularized zeta function, filled in at its pole by the positive class-number-formula residue.

    noncomputable def regularizedZeta (σ : ℝ) : ℝ :=
…
  2. lemma OAI.DukePrimeDegree.regularizedZeta_one line 26
  3. lemma OAI.DukePrimeDegree.regularizedZeta_one_pos line 30
  4. lemma OAI.DukePrimeDegree.regularizedZeta_of_ne_one line 33
  5. lemma OAI.DukePrimeDegree.regularizedZeta_continuousWithinAt_one line 38

    Source documentation

    Continuity at the residue from the half-plane of absolute convergence.

    lemma regularizedZeta_continuousWithinAt_one :
    ContinuousWithinAt (regularizedZeta K) (Ioi 1) 1 := by
…

    Mentions: OAI.DukePrimeDegree.regularizedZeta