OAI/Probability/FreeIsing/Gaussian/BinaryFusionMixture.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem367.binaryFusion_density_eq_mixtureline 12 - theorem
OAI.Problem367.linearSignalTilt_id_probabilityline 31 - theorem
OAI.Problem367.binaryFusionJointLaw_eq_conditional_mixtureline 39 - theorem
OAI.Problem367.binaryFusion_conditional_product_eq_tiltline 58