OAI/Analysis/KadisonKastler/PinchingRefinementInvariants.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two inequalities preserved by projection-family refinement

The total corner loss is charged to the test-vector displacement; the reference-vector displacement stays a prescribed small proportion of it.

  1. theorem OAI.KadisonKastler.partialPinching_refinement_preserves line 25