OAI/Probability/SKValue/GroundState/FiniteBranching.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValueG.finiteMaximum_div_pos line 12
2. lemma OAI.SKValueG.integral_scaled_gumbel_max line 23
3. lemma OAI.SKValueG.centered_gumbel_max line 34
4. theorem OAI.SKValueG.finite_branching_logheat_limit line 43
5. lemma OAI.SKValueG.iid_empiricalMean_L1 line 85
6. lemma OAI.SKValueG.nonnegative_L1_of_ae_and_integrals line 108
7. lemma OAI.SKValueG.empiricalMean_log_integrable line 135
8. theorem OAI.SKValueG.log_empiricalMean_L1 line 162