OAI/NumberTheory/DukePrimeDegree/Arithmetic/ZetaOrder.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A choice-independent continued zeta order

Zero orders do not depend on the ordering of the real embeddings or on the finite set of removed Euler factors. We fix one ordering only to package the continued zeta order as a function of a number field.

  1. theorem OAI.DukePrimeDegree.coset_analytic_off_zero_one line 25
  2. theorem OAI.DukePrimeDegree.coset_order_independent_of_data line 34
  3. def OAI.DukePrimeDegree.degreePred line 73
  4. theorem OAI.DukePrimeDegree.degreePred_spec line 75
  5. def OAI.DukePrimeDegree.canonicalRealEmbeddings line 81
  6. def OAI.DukePrimeDegree.zetaZeroOrder line 91

    Source documentation

    The zero order of the continued Dedekind zeta function, using a fixed embedding ordering and no removed primes.

    def zetaZeroOrder (K : Type*) [Field K] [NumberField K]
    [NumberField.IsTotallyReal K] (β : ℝ) : WithTop ℤ :=
…
  7. theorem OAI.DukePrimeDegree.zetaZeroOrder_eq_coset_order line 96
  8. theorem OAI.DukePrimeDegree.zetaZeroOrder_eq_completed_order line 102
  9. theorem OAI.DukePrimeDegree.zetaZeroOrder_finite_nonnegative line 109