OAI/Analysis/Cotype/TypeExtrapolation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.finite_geometric_sum_le line 12
2. theorem OAI.Cotype.normalized_type_bound_of_quadratic_powers line 30
3. theorem OAI.Cotype.nontrivialType_of_bConvex_nontrivial line 78
4. theorem OAI.Cotype.nontrivialType_of_bConvex line 88
5. theorem OAI.Cotype.nontrivialType_of_kConvex line 99
6. theorem OAI.Cotype.forwardTarget_proved line 102