OAI/Analysis/Cotype/BConvexQuantitative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.norm_rademacherSum_le_sum_norm line 10
2. theorem OAI.Cotype.exists_sign_norm_le_sum_sub line 18
3. theorem OAI.Cotype.average_sq_le_of_one_deficit line 61
4. theorem OAI.Cotype.rademacher_sq_le_of_sign_deficit line 79