OAI/Analysis/FreeEntropy/CumulantSeries.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.FreeSeries.Agree.mono line 12
  2. theorem OAI.FiniteEntropySeparation.FreeSeries.Agree.refl line 14
  3. theorem OAI.FiniteEntropySeparation.FreeSeries.Agree.symm line 15
  4. theorem OAI.FiniteEntropySeparation.FreeSeries.Agree.trans line 17
  5. theorem OAI.FiniteEntropySeparation.FreeSeries.agree_add line 19
  6. theorem OAI.FiniteEntropySeparation.FreeSeries.agree_deriv line 21
  7. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_agree line 24
  8. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_agree_left_step line 41
  9. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_left_cancel line 50
  10. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_injective line 65
  11. def OAI.FiniteEntropySeparation.FreeSeries.inverse line 76
  12. theorem OAI.FiniteEntropySeparation.FreeSeries.inverse_nil line 81
  13. theorem OAI.FiniteEntropySeparation.FreeSeries.inverse_cons line 82
  14. theorem OAI.FiniteEntropySeparation.FreeSeries.conv_inverse line 86
  15. theorem OAI.FiniteEntropySeparation.FreeSeries.inverse_conv line 91
  16. theorem OAI.FiniteEntropySeparation.FreeSeries.inverse_unique line 94
  17. theorem OAI.FiniteEntropySeparation.FreeSeries.inverse_inverse line 96
  18. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_inverse line 98
  19. def OAI.FiniteEntropySeparation.FreeSeries.momentIter line 103
  20. theorem OAI.FiniteEntropySeparation.FreeSeries.momentIter_nil line 107
  21. theorem OAI.FiniteEntropySeparation.FreeSeries.momentIter_step line 110
  22. theorem OAI.FiniteEntropySeparation.FreeSeries.momentIter_stable line 120
  23. def OAI.FiniteEntropySeparation.FreeSeries.moments line 126
  24. theorem OAI.FiniteEntropySeparation.FreeSeries.moments_agree line 127
  25. theorem OAI.FiniteEntropySeparation.FreeSeries.moments_nil line 131
  26. theorem OAI.FiniteEntropySeparation.FreeSeries.moments_eq line 132
  27. theorem OAI.FiniteEntropySeparation.FreeSeries.moments_unique line 138
  28. def OAI.FiniteEntropySeparation.FreeSeries.boolean line 154
  29. def OAI.FiniteEntropySeparation.FreeSeries.cumulants line 155
  30. theorem OAI.FiniteEntropySeparation.FreeSeries.boolean_nil line 157
  31. theorem OAI.FiniteEntropySeparation.FreeSeries.cumulants_nil line 158
  32. theorem OAI.FiniteEntropySeparation.FreeSeries.cumulants_equation line 160
  33. theorem OAI.FiniteEntropySeparation.FreeSeries.cumulants_unique line 184