OAI/Probability/FreeIsing/Conditioning/ObservationInformation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.map_observation_posterior_pair_eq_binaryFusionJointLaw line 26
2. theorem OAI.Problem367.condExp_observation_pair_map_eq_binaryFusion line 52
3. theorem OAI.Problem367.condExp_observation_pair_secondMoment line 68
4. theorem OAI.Problem367.condExp_observation_pair_secondMoment_le_add line 101
5. theorem OAI.Problem367.condExp_observation_pair_abs_lt_one line 116
6. theorem OAI.Problem367.condExp_observation_pair_neg_invariant line 125
7. theorem OAI.Problem367.condExp_observation_pair_secondMoment_le line 141