AlternatingNorm.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Complex norms after clearing an alternating-product denominator

The integral alternating product is related to its character values by a polynomial identity in the coefficient ring. Applying an arbitrary complex ring homomorphism to that identity is legitimate even before knowing that the homomorphism extends to the fraction field. Equal numbers of numerator and denominator factors, all of the same positive norm, then force norm one.

theorem OAI.CirculantHadamard.AlternatingNorm.norm_map_prod_of_const line 22

theorem OAI.CirculantHadamard.AlternatingNorm.norm_eq_one_of_balanced_products line 36

Source documentation

The numerator and denominator have equally many character factors. Only a genuine cleared identity in R is required; there is no assumed norm bound on z, no injectivity assumption on σ, and no fraction-field extension.

theorem norm_eq_one_of_balanced_products {R : Type uR} {ι : Type uIota} [CommRing R]
    (σ : R →+* ℂ) (x : ι → R) (numerator denominator : Finset ι)
    (z : R) (c : ℝ) (hc : 0 < c)
    (hcard : numerator.card = denominator.card)
    (hnumerator : ∀ i ∈ numerator, ‖σ (x i)‖ = c)
    (hdenominator : ∀ i ∈ denominator, ‖σ (x i)‖ = c)
    (hclear : z * (∏ i ∈ denominator, x i) = ∏ i ∈ numerator, x i) :
    ‖σ z‖ = 1 := by
…