OAI/Probability/FreeIsing/Gaussian/TreeResponse.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem367.GaussianTreeResponse.response line 16
2. lemma OAI.Problem367.GaussianTreeResponse.measurable_response line 20
3. lemma OAI.Problem367.GaussianTreeResponse.response_congr line 27
4. lemma OAI.Problem367.GaussianTreeResponse.response_erase line 39
5. lemma OAI.Problem367.GaussianTreeResponse.response_leaf line 47
6. lemma OAI.Problem367.GaussianTreeResponse.measurable_response_sq line 57
7. lemma OAI.Problem367.GaussianTreeResponse.response_updated_fields line 64
8. lemma OAI.Problem367.GaussianTreeResponse.lmarginal_leaf line 86
9. lemma OAI.Problem367.GaussianTreeResponse.lmarginal_nonleaf line 108
10. theorem OAI.Problem367.GaussianTreeResponse.lmarginal_response_sq_le line 126
11. theorem OAI.Problem367.GaussianTreeResponse.lintegral_gaussian_response_sq_le line 223
12. lemma OAI.Problem367.GaussianTreeResponse.integrable_response_sq line 243
13. theorem OAI.Problem367.GaussianTreeResponse.integral_gaussian_response_sq_le line 268