OAI/Combinatorics/Ryser/Probability/Exponential.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RyserCoveringCounterexample.FiniteLaw.expectation_mul_left_real line 15
2. lemma OAI.RyserCoveringCounterexample.FiniteLaw.exp_le_one_add_add_sq line 25
3. lemma OAI.RyserCoveringCounterexample.FiniteLaw.expectation_exp_le_of_mean_zero line 31
4. lemma OAI.RyserCoveringCounterexample.FiniteLaw.iterated_centered_mgf_le line 74
5. lemma OAI.RyserCoveringCounterexample.FiniteLaw.chernoff_upper line 122
6. lemma OAI.RyserCoveringCounterexample.FiniteLaw.chernoff_upper_of_mgf line 148
7. lemma OAI.RyserCoveringCounterexample.FiniteLaw.bernstein_scalar_optimization line 165
8. lemma OAI.RyserCoveringCounterexample.FiniteLaw.prob_abs_ge_le_add line 214
9. lemma OAI.RyserCoveringCounterexample.FiniteLaw.bernstein_abs_tail_of_mgf line 231