OAI/Analysis/KadisonKastler/FiniteFactorCommutantNear.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative commutant approximation for nearby finite factors

The constructed finite-factor estimate and the proved complete commutator-distance formula give the approximation needed to align reducing projections. No published perturbation input is used.

  1. theorem OAI.KadisonKastler.concreteDerivation_norm_le_of_commutant_near line 27
  2. theorem OAI.KadisonKastler.finiteFactor_commutant_approx_of_gap line 42