OAI/Probability/RadialTransition/MixtureBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RadialTransition.quadraticTerm line 14
2. lemma OAI.RadialTransition.quadraticTerm_pos line 17
3. lemma OAI.RadialTransition.quadraticTerm_tail_bound line 21
4. lemma OAI.RadialTransition.exp_neg_nat_summable line 48
5. lemma OAI.RadialTransition.exp_neg_positive_tail line 52
6. lemma OAI.RadialTransition.summable_of_tail_exp line 78
7. lemma OAI.RadialTransition.tail_le_one_of_exp line 91
8. lemma OAI.RadialTransition.truncated_sum_bound line 103