OAI/Analysis/KadisonKastler/CentralRefinementSequence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The increasing central-vector refinement sequence

Summable displacement budgets keep the limit vector nonzero. Successive finite tests give a single increasing matrix sequence with vanishing distance-to-line errors on the prescribed countable dense family.

  1. def OAI.KadisonKastler.centralRefinementIterates line 23
  2. theorem OAI.KadisonKastler.centralRefinementIterates_zero line 28
  3. theorem OAI.KadisonKastler.centralRefinementIterates_succ line 32
  4. theorem OAI.KadisonKastler.centralRefinementIterates_mono line 36
  5. theorem OAI.KadisonKastler.centralRefinementIterates_displacement line 45
  6. theorem OAI.KadisonKastler.central_refinement_sequence_of_refiners line 66
  7. theorem OAI.KadisonKastler.exists_central_refinement_sequence line 94