OAI/Probability/SKGap/Matrix/InverseSeries.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SKGap.Noncrossing.WordSeries.noiseSplitNilIsEmpty line 37
  2. def OAI.SKGap.Noncrossing.WordSeries.inverseSeries line 40
  3. def OAI.SKGap.Noncrossing.WordSeries.meanSeries line 42
  4. lemma OAI.SKGap.Noncrossing.WordSeries.coeff_inverseSeries line 43
  5. lemma OAI.SKGap.Noncrossing.WordSeries.coeff_meanSeries line 45
  6. lemma OAI.SKGap.Noncrossing.WordSeries.meanSeries_C line 48
  7. lemma OAI.SKGap.Noncrossing.WordSeries.coeff_mul_fin line 55
  8. lemma OAI.SKGap.Noncrossing.WordSeries.inverseSeries_right line 60
  9. lemma OAI.SKGap.Noncrossing.WordSeries.inverseSeries_left line 79
  10. def OAI.SKGap.Noncrossing.Letter.toWord line 112
  11. def OAI.SKGap.Noncrossing.liftWord line 115
  12. lemma OAI.SKGap.Noncrossing.liftWord_nil line 116
  13. lemma OAI.SKGap.Noncrossing.liftWord_cons line 117
  14. lemma OAI.SKGap.Noncrossing.liftWord_append line 119
  15. lemma OAI.SKGap.Noncrossing.inverseCount_lift line 120
  16. lemma OAI.SKGap.Noncrossing.exists_lift_of_no_inverse line 125
  17. lemma OAI.SKGap.Noncrossing.inverseCount_inverse line 139
  18. lemma OAI.SKGap.Noncrossing.one_inverse_cases line 142
  19. def OAI.SKGap.Noncrossing.expandWord line 163
  20. lemma OAI.SKGap.Noncrossing.expandWord_lift line 168
  21. lemma OAI.SKGap.Noncrossing.expandWord_oneInverse line 173
  22. def OAI.SKGap.Noncrossing.literalSeries line 180
  23. lemma OAI.SKGap.Noncrossing.literalSeries_lift line 183
  24. lemma OAI.SKGap.Noncrossing.literalSeries_oneInverse line 186
  25. instance OAI.SKGap.Noncrossing.noiseSplitDiagIsEmpty line 192
  26. instance OAI.SKGap.Noncrossing.noiseSplitNoiseUnique line 198
  27. lemma OAI.SKGap.Noncrossing.sum_noiseSplit_cons_diag line 206
  28. lemma OAI.SKGap.Noncrossing.sum_noiseSplit_cons_noise line 212
  29. lemma OAI.SKGap.Noncrossing.sum_wordPartners_lift line 220
  30. lemma OAI.SKGap.Noncrossing.sum_wordPartners_append line 238
  31. lemma OAI.SKGap.Noncrossing.sum_wordPartners_oneInverse line 251