OAI/Analysis/KadisonKastler/CentralContractionIteration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A fixed contraction gives arbitrary one-vector refinement

The reference vector may move by a summable prescribed amount. Each step contracts only the residual orthogonal to its current central line; projection onto the new line can only improve that estimate.

  1. theorem OAI.KadisonKastler.exists_central_refinement_geometric line 23
  2. theorem OAI.KadisonKastler.exists_central_refinement_of_contraction line 56