OAI/Analysis/KadisonKastler/ReducingCommutantNear.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Commutant approximation after aligning a reducing subspace

The finite-factor estimate is applied before moving the neighbor. This keeps the error linear in the original gap, with no repeated amplification constant after the unitary correction.

  1. theorem OAI.KadisonKastler.cornerCompression_mem_reducing_commutant line 22
  2. theorem OAI.KadisonKastler.reducing_commutant_approx_after_alignment line 34
  3. theorem OAI.KadisonKastler.nearInclusion_reducing_commutants_after_alignment line 80
  4. theorem OAI.KadisonKastler.reducing_commutant_reverse_approx_after_alignment line 100
  5. theorem OAI.KadisonKastler.reverse_nearInclusion_reducing_commutants_after_alignment line 148
  6. theorem OAI.KadisonKastler.kkDistance_reducing_commutants_after_alignment line 167