TypeIIICenteredImplementer.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Constructed norm bounds for type III inner implementers

theorem OAI.KadisonKastler.TypeIIIFactor.exists_centered_selfAdjoint_implementer line 19
Source documentation
Finite spectral averages center a self-adjoint implementer with the exact bound needed by normalizer factorization.
```
theorem TypeIIIFactor.exists_centered_selfAdjoint_implementer (hP : TypeIIIFactor P)
    (h : H →L[ℂ] H) (a : Algebra P) (ha : IsSelfAdjoint a)
    (hb : h - a.val ∈ P.commutant) :
    ∃ z : ℂ, ‖a.val - z • (1 : H →L[ℂ] H)‖ ≤ 2 * ‖h‖ := by
…
```
Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.TypeIIIFactor.exists_bounded_selfAdjoint_split line 46

Source documentation

A bounded centered splitting for a type III normalizer.

theorem TypeIIIFactor.exists_bounded_selfAdjoint_split (hP : TypeIIIFactor P)
    (h : selfAdjoint (H →L[ℂ] H)) (a : Algebra P) (ha : IsSelfAdjoint a)
    (hb : (h : H →L[ℂ] H) - a.val ∈ P.commutant) :
    ∃ a' b' : selfAdjoint (H →L[ℂ] H),
      (a' : H →L[ℂ] H) ∈ P ∧ (b' : H →L[ℂ] H) ∈ P.commutant ∧
      h = a' + b' ∧ ‖(a' : H →L[ℂ] H)‖ ≤ 2 * ‖(h : H →L[ℂ] H)‖ ∧
      ‖(b' : H →L[ℂ] H)‖ ≤ 3 * ‖(h : H →L[ℂ] H)‖ := by
…

Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.Algebra