DihedralPolynomialMoments.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The Haar and reflection-coset moments determine all polynomial moments of the real part of a dihedral rotation.

theorem OAI.KadisonSimilarity.realPart_mul_rotation line 16
theorem OAI.KadisonSimilarity.realPart_pow_mul_rotation line 30
def OAI.KadisonSimilarity.angularCharacter line 41
Source documentation
Angular characters with the sign convention of arcFourierIntegral.
```
def angularCharacter (l : ℤ) (x : ℝ) : ℂ :=
…
```
theorem OAI.KadisonSimilarity.angularCharacter_continuous line 44
theorem OAI.KadisonSimilarity.cosine_mul_angularCharacter line 48
def OAI.KadisonSimilarity.angularPowerMoment line 67
Source documentation
Normalized angular moments of powers of the real coordinate.
```
def angularPowerMoment (n : ℕ) (l : ℤ) : ℂ :=
…
```
theorem OAI.KadisonSimilarity.angularPowerMoment_zero line 71
theorem OAI.KadisonSimilarity.angularPowerMoment_succ line 82

theorem OAI.KadisonSimilarity.trace_realPart_pow_rotation line 108

Source documentation

The Haar law supplies precisely the scalar angular moments of the real part, including every shifted Fourier coefficient.

theorem trace_realPart_pow_rotation (τ : A →ₗ[ℂ] ℂ) (w : Aˣ)
    (hw : star (w : A) = (↑w⁻¹ : A))
    (hhaar : ∀ l : ℤ, τ (↑(w ^ l) : A) = if l = 0 then 1 else 0)
    (n : ℕ) (l : ℤ) :
    τ ((realPart (w : A) : A) ^ n * (↑(w ^ l) : A)) = angularPowerMoment n l := by
…

Mentions: OAI.KadisonSimilarity.angularPowerMoment

theorem OAI.KadisonSimilarity.trace_realPart_pow_rotation_reflection line 121

Source documentation

Vanishing on the entire reflection coset propagates to every polynomial in the real part.

theorem trace_realPart_pow_rotation_reflection (τ : A →ₗ[ℂ] ℂ) (w : Aˣ) (d : A)
    (hw : star (w : A) = (↑w⁻¹ : A))
    (hcoset : ∀ l : ℤ, τ ((↑(w ^ l) : A) * d) = 0) (n : ℕ) (l : ℤ) :
    τ (((realPart (w : A) : A) ^ n * (↑(w ^ l) : A)) * d) = 0 := by
…

theorem OAI.KadisonSimilarity.trace_realPart_polynomial_rotation line 131
theorem OAI.KadisonSimilarity.trace_realPart_polynomial_rotation_reflection line 158