OAI/Analysis/KadisonKastler/ConstructedPairedAmplification.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Complete closeness from the proved finite-factor estimate

  1. theorem OAI.KadisonKastler.constructed_complete_closeness_of_paired_factor line 26