OAI/Analysis/KadisonKastler/FiniteOrbitDistance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Operator distance from finite simultaneous orbit estimates

Finite coefficient factorization turns orbit-projection bounds into dual bounds. Weak operator separation then supplies norm approximants.

  1. theorem OAI.KadisonKastler.finite_orbit_dual_bound line 22
  2. theorem OAI.KadisonKastler.exists_near_algebra_of_finite_orbit_bound line 68