OAI/Probability/FreeIsing/Energy/MixedMoments.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.exists_two_positive_of_mixed line 8
2. theorem OAI.Problem367.mixed_sum_sq_le line 23
3. theorem OAI.Problem367.mixed_moment_product_le line 35
4. theorem OAI.Problem367.mixed_multinomial_sum_le line 63
5. theorem OAI.Problem367.independent_abs_moment_le_pure_add_remainder line 100