OAI/Analysis/FreeEntropy/WordSeries.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiniteEntropySeparation.FreeSeries.Series line 11
  2. def OAI.FiniteEntropySeparation.FreeSeries.unit line 13
  3. def OAI.FiniteEntropySeparation.FreeSeries.deriv line 17
  4. def OAI.FiniteEntropySeparation.FreeSeries.conv line 19
  5. theorem OAI.FiniteEntropySeparation.FreeSeries.unit_nil line 23
  6. theorem OAI.FiniteEntropySeparation.FreeSeries.unit_cons line 24
  7. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_nil line 25
  8. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_cons line 26
  9. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_apply line 28
  10. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_sum_splits line 30
  11. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_add_left line 40
  12. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_add_right line 43
  13. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_smul_left line 46
  14. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_smul_right line 49
  15. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_zero_left line 55
  16. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_zero_right line 58
  17. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_conv line 61
  18. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_unit line 63
  19. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_unit_left line 65
  20. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_unit_right line 68
  21. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_assoc line 74
  22. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_neg_left line 83
  23. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_neg_right line 85
  24. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_sub_left line 87
  25. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_sub_right line 89
  26. def OAI.FiniteEntropySeparation.FreeSeries.Agree line 92
  27. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_agree line 93
  28. theorem OAI.FiniteEntropySeparation.FreeSeries.length_induction line 102
  29. def OAI.FiniteEntropySeparation.FreeSeries.subst line 106
  30. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_nil line 111
  31. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_cons line 112
  32. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_subst line 115
  33. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_add line 120
  34. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_smul line 135
  35. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_zero line 150
  36. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_unit line 153
  37. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_mul line 159
  38. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_neg line 173
  39. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_sub line 175
  40. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_unit_left line 178
  41. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_comp line 184