OAI/Analysis/Cotype/ProjectionDeficit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.exists_norming_sum_deficit line 11
2. theorem OAI.Cotype.abs_prod_sign line 30
3. theorem OAI.Cotype.prod_sign_union_singleton line 36
4. theorem OAI.Cotype.projection_sign_sum_lower line 51
5. theorem OAI.Cotype.projection_complement_bound_of_sign_deficit line 96