OAI/Probability/SKGap/Matrix/MarkedWordIBP.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.matrix_marked_expand line 14
  2. theorem OAI.SKGap.goe_marked_sum_IBP line 22
  3. lemma OAI.SKGap.actualWord_append line 54
  4. lemma OAI.SKGap.actualWordDirection_append line 59
  5. lemma OAI.SKGap.matrix_word_contraction line 86
  6. lemma OAI.SKGap.matrix_word_reverse_bound line 105
  7. lemma OAI.SKGap.matrix_word_scaled_contraction line 112
  8. structure OAI.SKGap.WordCut line 132
  9. def OAI.SKGap.WordCut.prepend line 139
  10. def OAI.SKGap.wordPartners line 142
  11. lemma OAI.SKGap.wordPartners_cons line 150
  12. lemma OAI.SKGap.actualWord_nil line 159
  13. lemma OAI.SKGap.actualWord_cons line 161
  14. def OAI.SKGap.WordCut.value line 165
  15. lemma OAI.SKGap.WordCut.value_prepend line 170
  16. theorem OAI.SKGap.actualWordDirection_partners line 176
  17. def OAI.SKGap.ordinaryCount line 199
  18. def OAI.SKGap.inverseCount line 202
  19. lemma OAI.SKGap.wordPartners_counts line 206