OAI/Probability/FreeIsing/Gaussian/BinarySignalFusion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.condDistrib_raw_signal_likelihood line 16
2. theorem OAI.Problem367.posterior_version_calibrated line 63
3. theorem OAI.Problem367.condExp_raw_pair_eq_binaryFusion line 82
4. theorem OAI.Problem367.calibrated_condIndep_pair_law line 131
5. theorem OAI.Problem367.raw_condIndep_fusion_quadratic_loss line 158