OAI/Analysis/Cotype/IndependentSigns.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.average_comp_coordinate_embedding line 10
2. theorem OAI.Cotype.rademacherSum_extend line 29
3. theorem OAI.Cotype.sum_norm_sq_extend line 46
4. theorem OAI.Cotype.rademacher_sq_extend line 60
5. theorem OAI.Cotype.QuadraticTypeBound.mono_dim line 66
6. theorem OAI.Cotype.quadraticTypeBound_le_pow line 72
7. theorem OAI.Cotype.QuadraticTypeBound.support line 76