OAI/Probability/FreeIsing/Energy/NormalizedResponseLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.posteriorResponse line 14
2. lemma OAI.Problem367.stronglyMeasurable_posteriorResponse line 18
3. lemma OAI.Problem367.abs_covariance_le_variance_of_binary_moment_bounds line 24
4. theorem OAI.Problem367.ae_abs_posteriorCovariance_le_binary_variance line 38
5. theorem OAI.Problem367.ae_abs_posteriorResponse_le_one line 86
6. theorem OAI.Problem367.tendsto_ae_posteriorResponse line 102
7. theorem OAI.Problem367.tendsto_integral_sq_sub_posteriorResponse line 117