OAI/Probability/SKGap/Matrix/WordLoopLeading.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.actualWord_marked_integrable line 14
2. lemma OAI.SKGap.integrable_list_map_sum line 66
3. lemma OAI.SKGap.integral_list_sum_bound line 76
4. def OAI.SKGap.wordExpectedRecursion line 96
5. lemma OAI.SKGap.weighted_integral_error line 102
6. def OAI.SKGap.wordRecursionAtExpected line 110
7. def OAI.SKGap.wordRecursionAtCost line 115
8. theorem OAI.SKGap.actualWord_loop_leading line 121