OAI/Analysis/MarkovType/JConvexityScalarSquares.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.normalized_sum_sub_one_sq line 13
2. theorem OAI.MarkovSuperreflexivity.card_le_sum_sq_of_sum_eq line 28
3. theorem OAI.MarkovSuperreflexivity.card_add_sq_le_sum_sq_of_one_add_le line 36
4. theorem OAI.MarkovSuperreflexivity.sq_sum_le_card_mul_sum_sq line 47
5. theorem OAI.MarkovSuperreflexivity.sum_le_card_sub_one_mul_add line 52