FiniteSymmetrization.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Finite unitary averaging and weak-operator cluster points. These are the analytic and algebraic symmetrization steps, before identifying the matrix unitaries of the free-product model.

def OAI.KadisonSimilarity.finiteMean line 19
Source documentation
Uniform average over a nonempty finite set.
```
def finiteMean (f : Γ → V) : V := (Fintype.card Γ : ℂ)⁻¹ • ∑ g, f g
```
theorem OAI.KadisonSimilarity.finiteMean_const line 21
theorem OAI.KadisonSimilarity.finiteMean_sub line 27
theorem OAI.KadisonSimilarity.norm_finiteMean_le line 31
def OAI.KadisonSimilarity.finiteTwirl line 49
Source documentation
The twirl associated to a finite unitary representation. Its inverse is written using the group, so no adjoint identities are hidden in this definition.
```
def finiteTwirl (U : Γ →* (H →L[ℂ] H)) (T : H →L[ℂ] H) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.representation_mul_inv line 53
theorem OAI.KadisonSimilarity.representation_inv_mul line 57
theorem OAI.KadisonSimilarity.norm_finiteTwirl_le line 61
Source documentation
Contractivity of finite averaging of unitary conjugates.
```
theorem norm_finiteTwirl_le (U : Γ →* (H →L[ℂ] H))
    (hU : ∀ g, ‖U g‖ ≤ 1) (T : H →L[ℂ] H) : ‖finiteTwirl U T‖ ≤ ‖T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.finiteTwirl
theorem OAI.KadisonSimilarity.finiteTwirl_conjugate line 73
Source documentation
Reindexing the finite group proves exact invariance under its unitaries.
```
theorem finiteTwirl_conjugate (U : Γ →* (H →L[ℂ] H)) (T : H →L[ℂ] H) (g : Γ) :
    U g * finiteTwirl U T * U g⁻¹ = finiteTwirl U T := by
…
```
Mentions: OAI.KadisonSimilarity.finiteTwirl
theorem OAI.KadisonSimilarity.finiteTwirl_commute line 90
Source documentation
The averaged operator commutes with every unitary in the finite group.
```
theorem finiteTwirl_commute (U : Γ →* (H →L[ℂ] H)) (T : H →L[ℂ] H) (g : Γ) :
    commutator (finiteTwirl U T) (U g) = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.finiteTwirl

theorem OAI.KadisonSimilarity.norm_sub_finiteTwirl_le line 97

Source documentation

A bound on the original commutators bounds the distance to the twirl.

theorem norm_sub_finiteTwirl_le (U : Γ →* (H →L[ℂ] H))
    (hU : ∀ g, ‖U g‖ ≤ 1) (T : H →L[ℂ] H) {ε : ℝ}
    (hcomm : ∀ g, ‖commutator T (U g)‖ ≤ ε) : ‖T - finiteTwirl U T‖ ≤ ε := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.finiteTwirl

theorem OAI.KadisonSimilarity.conjugate_commutator line 123

Source documentation

Conjugation transports a commutator by an exact algebraic identity.

theorem conjugate_commutator (U : Γ →* (H →L[ℂ] H))
    (T A : H →L[ℂ] H) (g : Γ) :
    commutator (U g * T * U g⁻¹) A =
      U g * commutator T (U g⁻¹ * A * U g) * U g⁻¹ := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.scalarCommutatorNorm_finiteTwirl_le line 135

Source documentation

Twirling by unitaries in the algebra does not increase its scalar commutator seminorm.

theorem scalarCommutatorNorm_finiteTwirl_le (P : VonNeumannAlgebra H)
    (U : Γ →* (H →L[ℂ] H)) (hU : ∀ g, ‖U g‖ ≤ 1)
    (hmem : ∀ g, U g ∈ P) (T : H →L[ℂ] H) :
    scalarCommutatorNorm P (finiteTwirl U T) ≤ scalarCommutatorNorm P T := by
…

Mentions: OAI.KadisonSimilarity.scalarCommutatorNorm, OAI.KadisonSimilarity.finiteTwirl

theorem OAI.KadisonSimilarity.exists_weakOperator_cluster line 166

Source documentation

Every bounded sequence of operators has a weak-operator cluster point, without a separability assumption on the Hilbert space.

theorem exists_weakOperator_cluster (T : ℕ → H →L[ℂ] H) {R : ℝ} (hR : 0 ≤ R)
    (hbound : ∀ n, ‖T n‖ ≤ R) :
    ∃ S : H →L[ℂ] H, ‖S‖ ≤ R ∧ MapClusterPt (ofCLM S) atTop (fun n => ofCLM (T n)) := by
…

theorem OAI.KadisonSimilarity.norm_sub_le_of_weakOperator_cluster line 176

Source documentation

Operator-norm bounds on affine expressions pass to weak cluster points.

theorem norm_sub_le_of_weakOperator_cluster (T : ℕ → H →L[ℂ] H)
    (S A : H →L[ℂ] H)
    (hcluster : MapClusterPt (ofCLM S) atTop (fun n => ofCLM (T n)))
    {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ᶠ n in atTop, ‖T n - A‖ ≤ c) : ‖S - A‖ ≤ c := by
…

theorem OAI.KadisonSimilarity.norm_commutator_le_of_weakOperator_cluster line 186

Source documentation

Eventual commutator bounds pass to weak cluster points.

theorem norm_commutator_le_of_weakOperator_cluster (T : ℕ → H →L[ℂ] H)
    (S A : H →L[ℂ] H)
    (hcluster : MapClusterPt (ofCLM S) atTop (fun n => ofCLM (T n)))
    {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ᶠ n in atTop, ‖commutator (T n) A‖ ≤ c) :
    ‖commutator S A‖ ≤ c := by
…

Mentions: OAI.KadisonSimilarity.commutator