OAI/Analysis/Cotype/BConvexity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Cotype.BConvex line 11
2. theorem OAI.Cotype.exists_common_sign_norming line 15
3. theorem OAI.Cotype.l1Family_of_all_signs_large line 36
4. theorem OAI.Cotype.l1Family_of_not_bConvex line 61
5. theorem OAI.Cotype.uniformL1_of_not_bConvex line 75
6. theorem OAI.Cotype.bConvex_of_not_uniformL1 line 78