HaarSymmetrization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Haar symmetrization, defined through weak scalar integrals. This applies to the compact matrix-unitary actions used in the free-product argument.

def OAI.KadisonSimilarity.unitaryConjugate line 19

Source documentation

The orbit of a bounded operator under a representation.

def unitaryConjugate (U : Γ →* (H →L[ℂ] H)) (T : H →L[ℂ] H) (g : Γ) :
    H →L[ℂ] H := U g * T * U g⁻¹
…

theorem OAI.KadisonSimilarity.norm_unitaryConjugate_le line 23
def OAI.KadisonSimilarity.haarTwirl line 34
Source documentation
The Haar average is an actual bounded operator, with its weak integral constructed through Hilbert-space duality.
```
def haarTwirl (U : Γ →* (H →L[ℂ] H)) (hU : ∀ g, ‖U g‖ ≤ 1)
    (T : H →L[ℂ] H) (hI : WeaklyIntegrable μ (unitaryConjugate U T)) : H →L[ℂ] H :=
…
```
Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.unitaryConjugate
theorem OAI.KadisonSimilarity.norm_haarTwirl_le line 40
Source documentation
Haar averaging is contractive in operator norm.
```
theorem norm_haarTwirl_le (U : Γ →* (H →L[ℂ] H)) (hU : ∀ g, ‖U g‖ ≤ 1)
    (T : H →L[ℂ] H) (hI : WeaklyIntegrable μ (unitaryConjugate U T)) :
    ‖haarTwirl μ U hU T hI‖ ≤ ‖T‖ :=
…
```
Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.unitaryConjugate, OAI.KadisonSimilarity.haarTwirl
theorem OAI.KadisonSimilarity.haarTwirl_conjugate line 46
Source documentation
Left invariance of Haar measure gives invariance of the operator average.
```
theorem haarTwirl_conjugate (U : Γ →* (H →L[ℂ] H)) (hU : ∀ g, ‖U g‖ ≤ 1)
    (T : H →L[ℂ] H) (hI : WeaklyIntegrable μ (unitaryConjugate U T)) (g : Γ) :
    U g * haarTwirl μ U hU T hI * U g⁻¹ = haarTwirl μ U hU T hI := by
…
```
Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.unitaryConjugate, OAI.KadisonSimilarity.haarTwirl
theorem OAI.KadisonSimilarity.haarTwirl_commute line 63
Source documentation
Thus the Haar average commutes with the whole compact group.
```
theorem haarTwirl_commute (U : Γ →* (H →L[ℂ] H)) (hU : ∀ g, ‖U g‖ ≤ 1)
    (T : H →L[ℂ] H) (hI : WeaklyIntegrable μ (unitaryConjugate U T)) (g : Γ) :
    commutator (haarTwirl μ U hU T hI) (U g) = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.unitaryConjugate, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.haarTwirl

theorem OAI.KadisonSimilarity.norm_commutator_haarTwirl_le line 73

Source documentation

Every common commutator estimate for the orbit survives Haar averaging.

theorem norm_commutator_haarTwirl_le (U : Γ →* (H →L[ℂ] H))
    (hU : ∀ g, ‖U g‖ ≤ 1) (T : H →L[ℂ] H)
    (hI : WeaklyIntegrable μ (unitaryConjugate U T)) (B : H →L[ℂ] H)
    {c : ℝ} (hc : 0 ≤ c) (hcomm : ∀ g, ‖commutator (unitaryConjugate U T g) B‖ ≤ c) :
    ‖commutator (haarTwirl μ U hU T hI) B‖ ≤ c :=
…

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

theorem OAI.KadisonSimilarity.haarTwirl_compression line 83

Source documentation

On a subspace fixed pointwise by the group, compression is exactly preserved by averaging.

theorem haarTwirl_compression (U : Γ →* (H →L[ℂ] H)) (hU : ∀ g, ‖U g‖ ≤ 1)
    (hstar : ∀ g, (U g).adjoint = U g⁻¹)
    (T : H →L[ℂ] H) (hI : WeaklyIntegrable μ (unitaryConjugate U T))
    (J : K →L[ℂ] H) (hfix : ∀ g, (U g).comp J = J) :
    J.adjoint.comp ((haarTwirl μ U hU T hI).comp J) = J.adjoint.comp (T.comp J) := by
…

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