OAI/Probability/FreeIsing/Energy/CoupledAttenuation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.cavity_pair_sub_sq_le line 15
2. theorem OAI.Problem367.cavity_pair_sub_abs_le line 48
3. theorem OAI.Problem367.memLp_log_responseAttenuation line 79
4. theorem OAI.Problem367.centered_log_response_discrepancy_of_identDistrib line 86
5. theorem OAI.Problem367.integrable_cavity_pair_sub_sq line 102
6. theorem OAI.Problem367.integral_cavity_pair_sub_sq_le line 120
7. theorem OAI.Problem367.integral_cavity_log_discrepancy_sq_le line 157