OAI/Probability/FreeIsing/Energy/IndependentMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.integrable_prod_comp_of_iIndepFun line 9
2. theorem OAI.Problem367.integrable_sum_pow_of_iIndepFun line 29
3. theorem OAI.Problem367.integral_sum_pow_of_iIndepFun line 50
4. theorem OAI.Problem367.integral_abs_sum_pow_le_of_iIndepFun line 80
5. theorem OAI.Problem367.piAntidiag_pure_filter_eq line 99
6. theorem OAI.Problem367.multinomial_sum_eq_pure_add_mixed line 132