SpectralHalfBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Order bounds from the positive spectral half

theorem OAI.KadisonKastler.spectral_half_bounds line 24
Source documentation
The positive and negative spectral halves bound a self-adjoint operator by its norm times the corresponding projection.
```
theorem spectral_half_bounds (x : Algebra M) (hx : IsSelfAdjoint x) :
    let p := positiveSupport x
…
```
Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.norm_le_of_symmetric_scalar_bounds line 65

Source documentation

Symmetric scalar order bounds control the norm of a self-adjoint operator.

theorem norm_le_of_symmetric_scalar_bounds [Nontrivial H]
    (x : H →L[ℂ] H) (hx : IsSelfAdjoint x) (r : ℝ)
    (hl : -(algebraMap ℝ (H →L[ℂ] H) r) ≤ x)
    (hu : x ≤ algebraMap ℝ (H →L[ℂ] H) r) : ‖x‖ ≤ r := by
…