CyclicAverages.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Cyclic averages of the zero character

The same cyclic-subgroup coefficients used in the Artin permutation identity recover a sum of character values from their cyclic averages. For a linear character each such average detects the principal factor.

theorem OAI.DukePrimeDegree.sum_linearCharacter line 18

Source documentation

The sum of a finite linear character detects the principal character.

theorem sum_linearCharacter {C : Type*} [Group C] [Fintype C]
    (χ : C →* ℂˣ) :
    (∑ g, (χ g : ℂ)) = if χ = 1 then (Fintype.card C : ℂ) else 0 := by
…

theorem OAI.DukePrimeDegree.sum_eq_cyclic_sums line 42

Source documentation

Cyclic indicator coefficients recover the full sum from cyclic subgroup sums. This is the scalar counterpart of the permutation identity.

theorem sum_eq_cyclic_sums
    {G : Type*} [Group G] [Fintype G]
    (a : CyclicSubgroups G → ℤ)
    (ha : ∀ g : G, (∑ C, if g ∈ C.val then a C else 0) = 1)
    (f : G → ℂ) :
    (∑ g, f g) = ∑ C : CyclicSubgroups G, (a C : ℂ) * ∑ g : C.val, f g := by
…

Mentions: OAI.DukePrimeDegree.CyclicSubgroups