SpectralClipStar.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Adjoint compatibility of the continuous spectral cutoff

A two-by-two block argument transports continuous functional calculus through an intertwiner between selfadjoint elements. Applied twice to xx* and x*x, it shows that the cutoff commutes with adjoints. This provides the left-sided fourth-moment estimate from the right-sided one.

theorem OAI.KadisonKastler.cfc_blockDiagonal line 40

theorem OAI.KadisonKastler.cfc_selfAdjoint_intertwines line 68

Source documentation

Continuous real functional calculus respects an intertwiner of two selfadjoint elements.

theorem cfc_selfAdjoint_intertwines (a b x : A)
    (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hx : a * x = x * b)
    (f : ℝ → ℝ) (hf : Continuous f) :
    cfc f a * x = x * cfc f b := by
…

theorem OAI.KadisonKastler.abs_star_intertwines line 87
Source documentation
The absolute values satisfy the usual polar intertwining identity, without requiring the existence of a polar partial isometry.
```
theorem abs_star_intertwines (x : A) : CFC.abs (star x) * x = x * CFC.abs x := by
…
```
theorem OAI.KadisonKastler.star_spectralClip line 98
Source documentation
Clipping an adjoint is the adjoint of the same continuous cutoff.
```
theorem star_spectralClip {β : ℝ} (hβ : 0 < β) (x : A) :
    star (spectralClip β x) = spectralClip β (star x) := by
…
```
Mentions: OAI.KadisonKastler.spectralClip