FactorSpectralContraction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A uniform spectral contraction in every factor

theorem OAI.KadisonKastler.apply_real_smul line 17
theorem OAI.KadisonKastler.apply_real_scalar line 22

theorem OAI.KadisonKastler.norm_sub_midpoint_le line 27

Source documentation

The midpoint of a scalar order interval is within half its length.

theorem norm_sub_midpoint_le (x : H →L[ℂ] H) (hx : IsSelfAdjoint x)
    (a b : ℝ) (hl : a • (1 : H →L[ℂ] H) ≤ x)
    (hu : x ≤ b • (1 : H →L[ℂ] H)) :
    ‖x - ((a + b) / 2) • (1 : H →L[ℂ] H)‖ ≤ (b - a) / 2 := by
…

theorem OAI.KadisonKastler.exists_factor_spectral_contraction line 52
Source documentation
Projection comparison shrinks the norm radius of a self-adjoint operator by three quarters after subtracting a real scalar.
```
theorem exists_factor_spectral_contraction (hM : ScalarCenter M)
    (x : Algebra M) (hx : IsSelfAdjoint x) :
    ∃ (A : FiniteInnerAverage M) (c : ℝ),
      ‖A.apply x.val - c • (1 : H →L[ℂ] H)‖ ≤ (3 / 4 : ℝ) * ‖x‖ := by
…
```
Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage