OAI/Probability/FreeIsing/Spins/ObservationFusion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.observationFusionJointLaw line 13
2. theorem OAI.Problem367.ae_observation_pair_bounds line 17
3. theorem OAI.Problem367.observationFusionJointLaw_eq_mixture line 29
4. theorem OAI.Problem367.observationFusion_positive_product_eq_tilt line 48
5. theorem OAI.Problem367.condExp_spin_given_observation_pair_eq_binaryFusion line 70