SU2
Results named in Tau Ceti's TauCeti.RepresentationTheory.SU2 modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremThe Weyl character formula for SU(2)#
Away from the two points z = ±1 of the maximal
torus, where the Weyl denominator vanishes, the character of Symᵈ(ℂ²) at diag (z, z⁻¹) is the
quotient of the Weyl numerator by the Weyl denominator.
TauCeti.SU2.character_symPower_torusHom_eq_div (d : ℕ) {z : Circle} (hz : ↑z ^ 2 ≠ 1) :
(TauCeti.SU2.symPower d).character (TauCeti.SU2.torusHom z) =
(↑z ^ (d + 1) - (↑z)⁻¹ ^ (d + 1)) / (↑z - (↑z)⁻¹)
Lean
Formalized in Tau Ceti as TauCeti.SU2.character_symPower_torusHom_eq_div.
Other forms
The Weyl character formula in the angle parametrisation. Formalized in Tau Ceti as TauCeti.SU2.character_symPower_torusExp_eq_sin_div_sin.
TauCeti.SU2.character_symPower_torusExp_eq_sin_div_sin (d : ℕ) {θ : ℝ} (hθ : Real.sin θ ≠ 0) :
(TauCeti.SU2.symPower d).character (TauCeti.SU2.torusExp θ) =
↑(Real.sin ((↑d + 1) * θ) / Real.sin θ)
Sources
Uses 1 · Used by 1
TheoremThe Weyl integration formula for SU(2)#
For a continuous class function f on SU(2),
the integral of f against the Haar probability measure is the integral over the Weyl chamber
[0, π] of the maximal torus against the Weyl density (2π)⁻¹ · 4 sin²θ dθ:
∫ f dμ = (2π)⁻¹ ∫₀^π f (diag (e^{iθ}, e^{-iθ})) · 4 sin²θ dθ.
The Weyl factor 4 sin²θ = |e^{iθ} - e^{-iθ}|² is the squared modulus of the Weyl denominator,
and the density has total mass one (TauCeti.SU2.weyl_integration_formula_normalized).
TauCeti.SU2.weyl_integration_formula {f : TauCeti.SU2 → ℂ} (hf : Continuous f)
(hconj : ∀ (u g : TauCeti.SU2), f (u * g * u⁻¹) = f g) :
∫ (g : TauCeti.SU2), f g ∂TauCeti.haarProb TauCeti.SU2 =
1 / (2 * ↑Real.pi) * ∫ (θ : ℝ) in 0..Real.pi, f (TauCeti.SU2.torusExp θ) * ↑(4 * Real.sin θ ^ 2)
Uses 2
TheoremThe Weyl numerator identity#
Multiplying the weight string of Symᵈ(ℂ²) by the Weyl
denominator z - z⁻¹ telescopes to z^{d+1} - z^{-(d+1)}.
No hypothesis is needed on z: at the two points z = ±1 where the denominator vanishes both
sides are 0.
TauCeti.SU2.sub_inv_mul_character_symPower_torusHom (d : ℕ) (z : Circle) :
(↑z - (↑z)⁻¹) * (TauCeti.SU2.symPower d).character (TauCeti.SU2.torusHom z) =
↑z ^ (d + 1) - (↑z)⁻¹ ^ (d + 1)
Lean
Formalized in Tau Ceti as TauCeti.SU2.sub_inv_mul_character_symPower_torusHom.
Other forms
The Weyl numerator identity in the angle parametrisation. Formalized in Tau Ceti as TauCeti.SU2.sin_mul_character_symPower_torusExp.
TauCeti.SU2.sin_mul_character_symPower_torusExp (d : ℕ) (θ : ℝ) :
↑(Real.sin θ) * (TauCeti.SU2.symPower d).character (TauCeti.SU2.torusExp θ) =
↑(Real.sin ((↑d + 1) * θ))
Sources
Used by 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.