OAI/Probability/FreeIsing/Gaussian/BinaryPosteriorResponseBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.BinaryPosteriorResponseBound.covariance_le_variance_of_pair_bounds line 13
2. lemma OAI.Problem367.BinaryPosteriorResponseBound.condExp_abs_le_of_abs_le line 25
3. theorem OAI.Problem367.BinaryPosteriorResponseBound.abs_posteriorCovariance_le_one_sub_sq line 33
4. theorem OAI.Problem367.BinaryPosteriorResponseBound.abs_normalized_posteriorCovariance_le_one line 76
5. theorem OAI.Problem367.HasFreeIsingLaw.infiniteGibbsResponse_abs_le_one_gaussian line 96
6. theorem OAI.Problem367.HasFreeIsingLaw.infiniteGibbsResponse_abs_le_one_brownian line 120
7. theorem OAI.Problem367.HasFreeIsingLaw.memLp_infiniteGibbsResponse_brownian line 145
8. theorem OAI.Problem367.HasFreeIsingLaw.memLp_infiniteGibbsResponse_time_brownian line 170