OAI/Analysis/FreeEntropy/LinearSeries.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.FreeSeries.reparam line 12
  2. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_nil line 15
  3. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_cons line 16
  4. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_reparam line 18
  5. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_add line 21
  6. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_smul line 30
  7. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_zero line 39
  8. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_sum line 41
  9. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_unit line 47
  10. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_conv line 54
  11. theorem OAI.FiniteEntropySeparation.FreeSeries.rightDeriv_reparam line 66
  12. theorem OAI.FiniteEntropySeparation.FreeSeries.Cyclic.reparam line 86
  13. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_subst line 93
  14. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_moments line 109
  15. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_cumulants line 114
  16. def OAI.FiniteEntropySeparation.FreeSeries.restrict line 120
  17. theorem OAI.FiniteEntropySeparation.FreeSeries.restrict_conv line 121
  18. theorem OAI.FiniteEntropySeparation.FreeSeries.restrict_subst line 125
  19. theorem OAI.FiniteEntropySeparation.FreeSeries.restrict_moments line 139