SpectralMoments.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Power traces determine finite Euler products

Finite spectra are determined by all their power sums. This is the linear-algebra step that turns the cyclic character identities into identities of local Artin Euler factors.

theorem OAI.DukePrimeDegree.finite_weights_eq_zero_of_moments line 20
theorem OAI.DukePrimeDegree.weighted_euler_products_eq_of_moments line 33

theorem OAI.DukePrimeDegree.euler_det_products_eq_of_characters line 86

Source documentation

Equality of finite-group characters gives the corresponding local Euler-factor identity. The natural exponents permit denominator-cleared integer character relations.

theorem euler_det_products_eq_of_characters
    {I G : Type*} [Fintype I] [Group G] [Finite G]
    {V : I → Type*} [∀ i, AddCommGroup (V i)] [∀ i, Module ℂ (V i)]
    [∀ i, FiniteDimensional ℂ (V i)]
    (ρ : ∀ i, Representation ℂ G (V i)) (p q : I → ℕ)
    (h : ∀ g, (∑ i, (p i : ℂ) * (ρ i).character g) =
      ∑ i, (q i : ℂ) * (ρ i).character g)
    (g : G) (z : ℂ) :
    (∏ i, (LinearMap.id - z • ρ i g).det ^ p i) =
      ∏ i, (LinearMap.id - z • ρ i g).det ^ q i := by
…