OAI/Probability/FreeIsing/Spins/PosteriorFusion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.measure_eq_fair_spin_mixture line 14
2. theorem OAI.Problem367.map_posterior_pair_eq_binaryFusionJointLaw line 24
3. theorem OAI.Problem367.condExp_spin_given_posterior_pair_eq_binaryFusion line 72
4. theorem OAI.Problem367.condExp_posterior_pair_secondMoment_le line 120