OAI/Probability/SKGap/Matrix/WordPartnerContraction.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.matrix_word_contraction_left line 13
  2. def OAI.SKGap.markedContraction line 28
  3. def OAI.SKGap.WordCut.leftContraction line 31
  4. def OAI.SKGap.WordCut.rightContraction line 36
  5. lemma OAI.SKGap.WordCut.leftContraction_eq line 41
  6. lemma OAI.SKGap.WordCut.rightContraction_eq line 56
  7. lemma OAI.SKGap.partnerList_leftContract line 71
  8. lemma OAI.SKGap.partnerList_rightContract line 81
  9. theorem OAI.SKGap.actualWord_partner_contractions line 91
  10. lemma OAI.SKGap.ordinaryCount_append line 109
  11. lemma OAI.SKGap.inverseCount_append line 111
  12. lemma OAI.SKGap.ordinaryCount_noise line 113
  13. lemma OAI.SKGap.inverseCount_noise line 115
  14. lemma OAI.SKGap.wordPartners_inverse_sides line 118
  15. structure OAI.SKGap.WordRecursionTerm line 137
  16. def OAI.SKGap.WordCut.asLeft line 142
  17. def OAI.SKGap.WordCut.asRight line 144
  18. def OAI.SKGap.wordRecursionAt line 146
  19. lemma OAI.SKGap.wordRecursionAt_decreases line 149
  20. lemma OAI.SKGap.wordRecursionAt_one_inverse line 163
  21. def OAI.SKGap.firstNoiseSplit line 184
  22. lemma OAI.SKGap.firstNoiseSplit_some line 189
  23. lemma OAI.SKGap.firstNoiseSplit_none line 209
  24. def OAI.SKGap.wordRecursionTerms line 214
  25. lemma OAI.SKGap.wordRecursionTerms_decreases line 219
  26. lemma OAI.SKGap.wordRecursionTerms_one_inverse line 231
  27. def OAI.SKGap.wordDiagonal line 243
  28. def OAI.SKGap.wordPrediction line 246