StarkAverage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Recovering the fixed-field zero order from cyclic averages

This is the scalar form of Stark's descent: the same cyclic indicator coefficients recover both a class-function average and the zero order of the corresponding fixed-field zeta function.

theorem OAI.DukePrimeDegree.sum_eq_fixedFieldMultiplicity_of_cyclic_averages line 24

theorem OAI.DukePrimeDegree.no_odd_index_zero_sign line 55

Source documentation

A cyclicly linear zero-order sign function cannot have average one on an odd-index subgroup and average zero on the full Galois group.

theorem no_odd_index_zero_sign
    {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)
    (hcyclic : ∀ C : Subgroup (E ≃ₐ[F] E), IsCyclic C → ∃ χ : C →* ℝˣ,
      (∀ x : C, fixedFieldMultiplicity β (Subgroup.zpowers (x : E ≃ₐ[F] E)) =
        if χ x = 1 then 1 else 0) ∧
      fixedFieldMultiplicity β C = if χ = 1 then 1 else 0)
    (H : Subgroup (E ≃ₐ[F] E)) (hodd : Odd H.index)
    (hH : fixedFieldMultiplicity β H = 1)
    (hG : fixedFieldMultiplicity β (⊤ : Subgroup (E ≃ₐ[F] E)) = 0) : False := by
…

Mentions: OAI.DukePrimeDegree.fixedFieldMultiplicity