OAI/Analysis/Commutator/FreeHankelBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.FreeBlocks.concrete_hankel_assembly line 31
2. lemma OAI.Kadison.FreeBlocks.normalized_fejer_entry line 80
3. lemma OAI.Kadison.FreeBlocks.normalized_errors line 114
4. theorem OAI.Kadison.FreeBlocks.free_hankel_bound line 169