OAI/Probability/SpanningForest/USTPosteriorResponse.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.USTResponse.extendMarks line 13
2. lemma OAI.Problem336.USTResponse.extendMarks_coe line 16
3. lemma OAI.Problem336.USTResponse.bit_finiteTreeConfiguration line 19
4. lemma OAI.Problem336.USTResponse.sum_restrict_support line 24
5. lemma OAI.Problem336.USTResponse.finiteEnergy_eq_observationField line 34
6. lemma OAI.Problem336.USTResponse.exp_finiteEnergy_eq_weight line 50
7. lemma OAI.Problem336.USTResponse.tiltedMean_finiteUSTProbability line 57
8. lemma OAI.Problem336.USTResponse.finiteTiltMean_eq_weight_ratio line 73
9. theorem OAI.Problem336.USTResponse.finiteTiltMean_eq_finiteTilt line 84
10. theorem OAI.Problem336.USTResponse.finiteUST_posterior_response_of_response line 103
11. theorem OAI.Problem336.USTResponse.finiteUST_posterior_response line 119
12. theorem OAI.Problem336.USTResponse.finiteUST_limit_posterior_response line 133