OAI/Probability/FreeIsing/Posterior/InfinitePosteriorField.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.finiteObservation line 21
2. theorem OAI.Problem367.measurable_finiteObservation line 25
3. theorem OAI.Problem367.gaussianPlanted_restrict_joint_law line 29
4. theorem OAI.Problem367.HasFreeIsingLaw.finiteObservation_condExp line 63
5. theorem OAI.Problem367.finiteIsingPosterior_tanh_bounds line 84
6. theorem OAI.Problem367.HasFreeIsingLaw.finiteObservation_spin_tanh_bounds line 120
7. def OAI.Problem367.finiteObservationFiltration line 141
8. theorem OAI.Problem367.finiteObservationFiltration_iSup line 155
9. theorem OAI.Problem367.HasFreeIsingLaw.posterior_field_bound_of_exhaustion line 175
10. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_posterior_field_bound line 197