OAI/Probability/SKValue/GroundState/GumbelMax.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValueG.finiteMaximum_le_iff line 13
2. def OAI.SKValueG.logSumExp line 19
3. lemma OAI.SKValueG.exp_sum_pos line 22
4. lemma OAI.SKValueG.gumbel_shift_cdf line 25
5. lemma OAI.SKValueG.gumbel_max_cdf line 32
6. theorem OAI.SKValueG.gumbel_max_law line 56
7. lemma OAI.SKValueG.gumbel_max_integrable line 69
8. lemma OAI.SKValueG.integral_gumbel_max line 80
9. lemma OAI.SKValueG.log_tangent_bound line 100
10. lemma OAI.SKValueG.log_mean_lower line 106
11. lemma OAI.SKValueG.integral_log_le_log_integral line 125