OAI/Probability/SKValue/GroundState/BranchMeanUpper.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValueG.branchMax_gumbelMean line 13
2. theorem OAI.SKValueG.branchLaw_mean_upper line 31
3. def OAI.SKValueG.gumbelTreeMoment line 84
4. lemma OAI.SKValueG.gumbelTreeMoment_pos line 88
5. lemma OAI.SKValueG.exp_prod_integrable_of_bound line 97
6. lemma OAI.SKValueG.fieldChildLaw_exp_bound line 114
7. theorem OAI.SKValueG.fieldTreeEval_moment_bound line 142
8. def OAI.SKValueG.gumbelTreeMean line 175
9. theorem OAI.SKValueG.fieldTreeEval_mean_upper line 179