OAI/Analysis/KadisonKastler/MatrixCentralRefinement.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Passing central-vector refinement estimates to finite families

Further matrix refinement preserves every previous distance-to-line estimate. Repeated one-vector refinement therefore handles any finite family with a prescribed total displacement budget.

  1. def OAI.KadisonKastler.matrixStageCentralProjection line 21
  2. theorem OAI.KadisonKastler.matrixStageCentralProjection_error_mono line 24
  3. theorem OAI.KadisonKastler.exists_finite_central_refinement line 40