CompactHaarIntegrability.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Strong continuity of a unitary action gives every weak Haar integral used in symmetrization. No continuity in operator norm is required.

theorem OAI.KadisonSimilarity.continuous_unitaryConjugate_coefficient line 21
Source documentation
Moving the left unitary to the second inner-product slot makes matrix coefficients of its conjugation action continuous in the strong topology.
```
theorem continuous_unitaryConjugate_coefficient
    (U : Γ →* (H →L[ℂ] H)) (hstar : ∀ g, (U g).adjoint = U g⁻¹)
    (hcont : ∀ x, Continuous (fun g => U g x)) (T : H →L[ℂ] H) (x y : H) :
    Continuous (fun g => inner ℂ (unitaryConjugate U T g x) y) := by
…
```
Mentions: OAI.KadisonSimilarity.unitaryConjugate

theorem OAI.KadisonSimilarity.weaklyIntegrable_unitaryConjugate line 36

Source documentation

On a compact group these continuous scalar coefficients are integrable against Haar probability measure.

theorem weaklyIntegrable_unitaryConjugate (μ : Measure Γ) [IsFiniteMeasure μ]
    (U : Γ →* (H →L[ℂ] H)) (hstar : ∀ g, (U g).adjoint = U g⁻¹)
    (hcont : ∀ x, Continuous (fun g => U g x)) (T : H →L[ℂ] H) :
    WeaklyIntegrable μ (unitaryConjugate U T) := by
…

Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.unitaryConjugate