SubfieldOrders.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Integer zero orders of fixed fields

The actual continued Dedekind zeta functions have finite nonnegative orders at real points between zero and one. Permutation character identities therefore give ordinary integer relations on these orders.

def OAI.DukePrimeDegree.zetaMultiplicity line 20
Source documentation
An integer-valued version of the continued zeta order.
```
def zetaMultiplicity (K : Type*) [Field K] [NumberField K]
    [NumberField.IsTotallyReal K] (β : ℝ) : ℤ :=
…
```
theorem OAI.DukePrimeDegree.zetaZeroOrder_eq_multiplicity line 24
theorem OAI.DukePrimeDegree.zetaMultiplicity_nonneg line 32
def OAI.DukePrimeDegree.fixedFieldMultiplicity line 48
theorem OAI.DukePrimeDegree.fixedFieldMultiplicity_conjugate line 51

theorem OAI.DukePrimeDegree.fixedFieldMultiplicity_relation line 61

Source documentation

An integer permutation-character relation gives the identical relation on the orders of the corresponding fixed-field zeta functions.

theorem fixedFieldMultiplicity_relation
    {I : Type*} [Fintype I] (H : I → Subgroup (E ≃ₐ[F] E)) (c : I → ℤ)
    (hχ : ∀ g, (∑ i, (c i : ℂ) * (Representation.ofMulAction ℂ (E ≃ₐ[F] E)
      ((E ≃ₐ[F] E) ⧸ H i)).character g) = 0)
    {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1) :
    (∑ i, c i * fixedFieldMultiplicity β (H i)) = 0 := by
…

Mentions: OAI.DukePrimeDegree.fixedFieldMultiplicity

theorem OAI.DukePrimeDegree.fixedFieldMultiplicity_cyclic_relation line 84

Source documentation

Cyclic induction inside a subgroup controls the zero order of its fixed field, including nonnormal intermediate fields.

theorem fixedFieldMultiplicity_cyclic_relation
    (H : Subgroup (E ≃ₐ[F] E)) (b : CyclicSubgroups H → ℤ)
    (hb : ∀ g : E ≃ₐ[F] E,
      (∑ C, (b C : ℂ) * (Representation.ofMulAction ℂ (E ≃ₐ[F] E)
        ((E ≃ₐ[F] E) ⧸ C.val.map H.subtype)).character g) =
      Fintype.card H * (Representation.ofMulAction ℂ (E ≃ₐ[F] E)
        ((E ≃ₐ[F] E) ⧸ H)).character g)
    {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1) :
    (∑ C, b C * fixedFieldMultiplicity β (C.val.map H.subtype)) =
      Fintype.card H * fixedFieldMultiplicity β H := by
…

Mentions: OAI.DukePrimeDegree.CyclicSubgroups, OAI.DukePrimeDegree.fixedFieldMultiplicity