OAI/Probability/FreeIsing/Ising/ObservationPosteriorTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.IsingObservationInnovation.measurePreserving_uniformObservation line 11
2. theorem OAI.Problem367.IsingObservationInnovation.measurable_posterior line 17
3. theorem OAI.Problem367.IsingObservationInnovation.posterior_memLp line 22
4. theorem OAI.Problem367.IsingObservationInnovation.posterior_uniformObservation line 29
5. theorem OAI.Problem367.IsingObservationInnovation.integral_posterior_pair_eq_uniform line 38
6. theorem OAI.Problem367.IsingObservationInnovation.integral_posterior_sub_sq_eq_uniform line 63