SpectralCommutant.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Spectral commutation for real character multipliers

Character commutation passes to every unitary of their commutant. Finite vector measures then give scalar-multiplier commutation, and the linear span of unitaries gives the assertion for every operator.

theorem OAI.KadisonKastler.regularCharacterUnitary_neg line 22

theorem OAI.KadisonKastler.commute_map_of_unitaries line 29

Source documentation

Commutation on the unitary generators extends by their linear span.

theorem commute_map_of_unitaries {A B : Type*} [CStarAlgebra A] [CStarAlgebra B]
    (f : A →⋆ₐ[ℂ] B) (T : B)
    (h : ∀ u : unitary A, Commute (f u) T) (a : A) : Commute (f a) T := by
…

def OAI.KadisonKastler.characterCommutant line 44
Source documentation
The closed C-star algebra commuting with all real character multipliers.
```
def characterCommutant :
    StarSubalgebra ℂ (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
instance OAI.KadisonKastler.characterCommutantCStarAlgebra line 50
theorem OAI.KadisonKastler.mem_characterCommutant line 53
theorem OAI.KadisonKastler.characterCommutant_unitary_commutes line 63
theorem OAI.KadisonKastler.commute_scalarMultiplier_of_characters line 71
theorem OAI.KadisonKastler.publishedRealSpectralCommutant line 86
Source documentation
The concrete real-line specialization of Stone's spectral commutant theorem cited in the downstream regular-core construction.
```
theorem publishedRealSpectralCommutant : PublishedRealSpectralCommutant.{u} := by
…
```