OAI/Probability/FreeIsing/Ising/ObservationLaw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Problem367.IsingObservationInnovation.observationLaw_probability line 11
2. theorem OAI.Problem367.IsingObservationInnovation.measurePreserving_observationLaw_relabel line 20
3. def OAI.Problem367.IsingObservationInnovation.past line 30
4. theorem OAI.Problem367.IsingObservationInnovation.measurable_past line 33
5. theorem OAI.Problem367.IsingObservationInnovation.filtration_eq_comap_past line 37
6. theorem OAI.Problem367.IsingObservationInnovation.filtration_comap_uniformObservation line 41