OAI/Probability/SKValue/GroundState/GumbelReplacement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValueG.lipschitz_integrable_comp line 12
2. def OAI.SKValueG.gumbelSmooth line 24
3. lemma OAI.SKValueG.gumbelSmooth_lipschitz line 27
4. lemma OAI.SKValueG.integral_comp_diff_le line 39
5. lemma OAI.SKValueG.scaled_gumbel_test_integral line 54
6. theorem OAI.SKValueG.marked_branching_limit line 79