OAI/Probability/SKGap/Brownian/GibbsContinuity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.continuous_weight line 13
2. lemma OAI.SKGap.continuous_partition line 17
3. lemma OAI.SKGap.continuous_mass line 21
4. lemma OAI.SKGap.continuous_expectation line 24
5. lemma OAI.SKGap.continuous_conditionalExpectation line 28
6. lemma OAI.SKGap.continuous_variance line 36
7. lemma OAI.SKGap.continuous_dirichlet line 42
8. lemma OAI.SKGap.terminal_goodSet_closed line 50
9. lemma OAI.SKGap.mass_le_one line 57
10. lemma OAI.SKGap.expectation_abs_le line 61
11. lemma OAI.SKGap.conditionalExpectation_abs_le line 69
12. lemma OAI.SKGap.conditionalExpectation_invariant line 79
13. lemma OAI.SKGap.conditionalExpectation_minimal line 87