OAI/Probability/FreeIsing/Energy/MomentTail.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem367.exists_moment_orderline 11 - theorem
OAI.Problem367.measureReal_abs_gt_le_momentline 39 - theorem
OAI.Problem367.measureReal_abs_gt_exp_le_of_momentsline 56 - theorem
OAI.Problem367.measureReal_abs_gt_rpow_le_of_momentsline 78 - theorem
OAI.Problem367.measure_abs_gt_rpow_le_of_momentsline 98