OAI/Analysis/KadisonKastler/StrictPinchingRefinement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A strict admissible refinement of every nearly full remainder

Both quantitative invariants survive the split, and the test-vector energy increases strictly. This is the local contradiction for a maximal orthogonal projection family.

  1. theorem OAI.KadisonKastler.exists_strict_pinching_refinement line 24