CentralCStarSource.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A norm-separable commutative C-star source for the center. Its commutant is the full central commutant, so its common spectral fields apply to every operator required by the central-decomposition estimate.

theorem OAI.KadisonSimilarity.central_subalgebra_isMulCommutative line 16

Source documentation

Every star subalgebra of the center is commutative.

theorem central_subalgebra_isMulCommutative (P : VonNeumannAlgebra H)
    (A : StarSubalgebra ℂ (H →L[ℂ] H)) (hA : A ≤ (vonNeumannCenter P).toStarSubalgebra) :
    IsMulCommutative A := by
…

Mentions: OAI.KadisonSimilarity.vonNeumannCenter

theorem OAI.KadisonSimilarity.subtype_star_range line 24
Source documentation
The source inclusion has exactly its original star subalgebra as range.
```
theorem subtype_star_range (A : StarSubalgebra ℂ (H →L[ℂ] H)) :
    A.subtype.range = A := by
…
```

theorem OAI.KadisonSimilarity.central_source_commutant line 34

Source documentation

A weakly generating central source has the full central commutant.

theorem central_source_commutant (P : VonNeumannAlgebra H)
    (A : StarSubalgebra ℂ (H →L[ℂ] H))
    (hgen : (starSubalgebraCommutant A).commutant = vonNeumannCenter P) :
    starSubalgebraCommutant A = (vonNeumannCenter P).commutant := by
…

Mentions: OAI.KadisonSimilarity.starSubalgebraCommutant, OAI.KadisonSimilarity.vonNeumannCenter

theorem OAI.KadisonSimilarity.exists_separable_central_source line 43

Source documentation

Choose only a norm-separable source; the center itself need not be norm separable.

theorem exists_separable_central_source [TopologicalSpace.SeparableSpace H]
    (P : VonNeumannAlgebra H) :
    ∃ A : StarSubalgebra ℂ (H →L[ℂ] H),
      IsClosed (A : Set (H →L[ℂ] H)) ∧ TopologicalSpace.SeparableSpace A ∧
      IsMulCommutative A ∧ A ≤ (vonNeumannCenter P).toStarSubalgebra ∧
      starSubalgebraCommutant A = (vonNeumannCenter P).commutant := by
…

Mentions: OAI.KadisonSimilarity.vonNeumannCenter, OAI.KadisonSimilarity.starSubalgebraCommutant