OAI/Probability/FreeIsing/Conditioning/FiniteBayesCondExp.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.FiniteBayes.condExp_state_eq_posterior_integral line 15
2. theorem OAI.Problem367.FiniteBayes.condExp_state_eq_real_likelihood line 33
3. theorem OAI.Problem367.FiniteBayes.condExp_state_eq_exponential_likelihood line 45
4. theorem OAI.Problem367.FiniteBayes.condDistrib_eq_posterior_of_joint_law line 66
5. theorem OAI.Problem367.FiniteBayes.condExp_state_eq_posterior_integral_of_joint_law line 77
6. theorem OAI.Problem367.FiniteBayes.condExp_state_eq_of_posterior_integral line 94