OAI/Probability/FreeIsing/Posterior/ProjectedObservationRecovery.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.measurable_time_copy_fst line 14
2. theorem OAI.Problem367.measurable_time_copy_snd line 21
3. theorem OAI.Problem367.conditionalCopies_ae_eq_projected line 28
4. theorem OAI.Problem367.isFactorOfIID_of_projected_observation_conditionalCopies line 41
5. theorem OAI.Problem367.isFactorOfIID_of_projected_observation_reference_collapse line 88
6. theorem OAI.Problem367.isFactorOfIID_of_projected_innovation_field_zero line 137
7. theorem OAI.Problem367.isFactorOfIID_of_innovation_comparison line 172