CentralSymmetrization.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Averaging over finite families of central projections

The finite sign groups and their averages are constructed explicitly. A weak operator cluster point of the net indexed by finite projection families commutes with every central projection. The final passage to the whole center uses only the already stated spectral-step specialization of Blackadar.

def OAI.KadisonSimilarity.vonNeumannCenter line 27
Source documentation
The center as a concrete von Neumann algebra.
```
def vonNeumannCenter (P : VonNeumannAlgebra H) : VonNeumannAlgebra H where
…
```
theorem OAI.KadisonSimilarity.mem_vonNeumannCenter line 42
def OAI.KadisonSimilarity.CentralProjection line 46
Source documentation
The projection index is unrestricted in cardinality.
```
def CentralProjection (P : VonNeumannAlgebra H) :=
…
```
def OAI.KadisonSimilarity.centralUnitarySubgroup line 49
theorem OAI.KadisonSimilarity.centralUnitary_commute line 58
def OAI.KadisonSimilarity.centralReflection line 66
theorem OAI.KadisonSimilarity.centralReflection_square line 75
theorem OAI.KadisonSimilarity.intUnit_eq_one_or_neg_one line 85
def OAI.KadisonSimilarity.centralSignHom line 88
def OAI.KadisonSimilarity.centralSignRepresentation line 97
theorem OAI.KadisonSimilarity.centralSignRepresentation_mem line 104
theorem OAI.KadisonSimilarity.norm_centralSignRepresentation_le line 110
theorem OAI.KadisonSimilarity.centralSignRepresentation_single line 120
def OAI.KadisonSimilarity.centralProjectionTwirl line 128
Source documentation
The finite average belonging to a finite family of central projections.
```
def centralProjectionTwirl (P : VonNeumannAlgebra H) (Y : H →L[ℂ] H)
    (s : Finset (CentralProjection P)) : H →L[ℂ] H :=
…
```
Mentions: OAI.KadisonSimilarity.CentralProjection
theorem OAI.KadisonSimilarity.centralProjectionTwirl_commute line 132

theorem OAI.KadisonSimilarity.exists_weakOperator_net_cluster line 148

Source documentation

Weak-operator compactness applies to arbitrary directed nets.

theorem exists_weakOperator_net_cluster {J : Type*} (l : Filter J) [l.NeBot]
    (T : J → H →L[ℂ] H) {R : ℝ} (hR : 0 ≤ R) (hbound : ∀ j, ‖T j‖ ≤ R) :
    ∃ S : H →L[ℂ] H, ‖S‖ ≤ R ∧ MapClusterPt (ofCLM S) l (fun j => ofCLM (T j)) := by
…

theorem OAI.KadisonSimilarity.norm_sub_le_of_weakOperator_net_cluster line 157
theorem OAI.KadisonSimilarity.norm_commutator_le_of_weakOperator_net_cluster line 166
theorem OAI.KadisonSimilarity.exists_central_projection_symmetrization line 178
Source documentation
No countability assumption is needed: finite sign averages have a common weak cluster point commuting with every central projection.
```
theorem exists_central_projection_symmetrization (P : VonNeumannAlgebra H)
    (Y : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hscalar : scalarCommutatorNorm P Y ≤ δ) :
    ∃ Y₁ : H →L[ℂ] H, ‖Y₁‖ ≤ ‖Y‖ ∧ ‖Y₁ - Y‖ ≤ δ ∧
      (∀ p : CentralProjection P, commutator Y₁ p.val = 0) := by
…
```
Mentions: OAI.KadisonSimilarity.scalarCommutatorNorm, OAI.KadisonSimilarity.CentralProjection, OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.commutator_zero_of_spectralSteps line 212

Source documentation

Norm approximation by spectral steps extends projection commutation to commutation with the whole von Neumann algebra.

theorem commutator_zero_of_spectralSteps (C : VonNeumannAlgebra H)
    (approximation : SpectralStepApproximation C) (T : H →L[ℂ] H)
    (hprojection : ∀ p : H →L[ℂ] H, p ∈ C → IsStarProjection p → commutator T p = 0) :
    ∀ a : H →L[ℂ] H, a ∈ C → commutator T a = 0 := by
…

Mentions: OAI.KadisonSimilarity.SpectralStepApproximation, OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.exists_central_symmetrization line 267
Source documentation
Central averaging for the global reduction. The only published input is spectral approximation inside the actual center; the average, its norm control, and its exact central commutation are all constructed above.
```
theorem exists_central_symmetrization (P : VonNeumannAlgebra H)
    (approximation : SpectralStepApproximation (vonNeumannCenter P))
    (Y : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hscalar : scalarCommutatorNorm P Y ≤ δ) :
    ∃ Y₁ : H →L[ℂ] H, ‖Y₁‖ ≤ ‖Y‖ ∧ ‖Y₁ - Y‖ ≤ δ ∧
      scalarCommutatorNorm P Y₁ ≤ 3 * δ ∧
      ∀ a : H →L[ℂ] H, a ∈ vonNeumannCenter P → commutator Y₁ a = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.SpectralStepApproximation, OAI.KadisonSimilarity.vonNeumannCenter, OAI.KadisonSimilarity.scalarCommutatorNorm, OAI.KadisonSimilarity.commutator