The Weyl integration formula for SU(2)

For a continuous class function f on SU(2), integration against the Haar probability measure reduces to an 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.

Purpose

The formula applies to continuous conjugation-invariant functions and uses Haar probability measure on SU(2). Its Weyl-chamber density has total mass one, as recorded by TauCeti.SU2.weyl_integration_formula_normalized. Specializing the formula to products of symmetric-power characters gives their Haar orthonormality in TauCeti.SU2.integral_character_symPower_mul_conj.

Main results

• TauCeti.SU2.integral_character_symPower: ∫ χ_d dμ = δ_{d0}.
• TauCeti.SU2.weyl_integration_formula: the Weyl integration formula for SU(2), for continuous class functions.
• TauCeti.SU2.integral_character_symPower_mul_conj: the characters of SU(2) are orthonormal, ∫ χ_m · conj χ_n dμ = δ_{mn}.

References

• D. Bump, Lie Groups, 2nd ed., Springer GTM 225 (2013), Chapters 17-18.
• T. Bröcker, T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter IV, §1.

The Haar integral of a character

@[simp]

theorem TauCeti.SU2.integral_character_symPower (d : ℕ) : ∫ (g : SU2), (symPower d).character g ∂haarProb SU2 = if d = 0 then 1 else 0

The Haar integral of the character of Symᵈ(ℂ²) is δ_{d0}. It is the dimension of the invariants: the whole line for the trivial representation Sym⁰(ℂ²), and nothing otherwise, since Symᵈ(ℂ²) is irreducible of dimension d + 1.

The Weyl-chamber functional

The Weyl integration formula

theorem TauCeti.SU2.weyl_integration_formula {f : SU2 → ℂ} (hf : Continuous f) (hconj : ∀ (u g : SU2), f (u * g * u⁻¹) = f g) : ∫ (g : SU2), f g ∂haarProb SU2 = 1 / (2 * ↑Real.pi) * ∫ (θ : ℝ) in 0..Real.pi, f (torusExp θ) * ↑(4 * Real.sin θ ^ 2)

The 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).

@[simp]

theorem TauCeti.SU2.integral_character_symPower_mul_conj (m n : ℕ) : ∫ (g : SU2), (symPower m).character g * (starRingEnd ℂ) ((symPower n).character g) ∂haarProb SU2 = if m = n then 1 else 0

The characters of SU(2) are orthonormal against Haar measure: ∫ χ_m · conj χ_n dμ = δ_{mn} for the characters χ_d of the symmetric powers Symᵈ(ℂ²).

The Weyl integration formula TauCeti.SU2.weyl_integration_formula moves the integral to the Weyl chamber, where it is TauCeti.SU2.character_symPower_orthonormal_torusExp.