OAI/Analysis/Cotype/KConvexUniformL1.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.radProjection_kernel line 11
2. theorem OAI.Cotype.scalar_sign_row_L2 line 24
3. theorem OAI.Cotype.radProjection_l1Family_pointwise line 30
4. theorem OAI.Cotype.sqrt_le_of_kBound_l1Family line 51
5. theorem OAI.Cotype.not_uniformL1_of_kConvex line 64