OAI/Analysis/Cotype/L2Sequence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.lp_two_summable_sq line 14
2. theorem OAI.Cotype.lp_two_norm_sq line 18
3. theorem OAI.Cotype.mem_lp_two_of_summable_sq line 22
4. theorem OAI.Cotype.cubeL2_lp_sq line 28
5. theorem OAI.Cotype.norm_sq_le_card_cubeL2_sq line 35