OAI/Analysis/FreeEntropy/EmbeddedSeries.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.FreeSeries.liftSeries line 10
  2. theorem OAI.FiniteEntropySeparation.FreeSeries.liftSeries_nil line 11
  3. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_liftSeries line 12
  4. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_liftSeries_image line 15
  5. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_liftSeries_out line 20
  6. theorem OAI.FiniteEntropySeparation.FreeSeries.liftSeries_letter line 24
  7. theorem OAI.FiniteEntropySeparation.FreeSeries.restrict_liftSeries line 36
  8. theorem OAI.FiniteEntropySeparation.FreeSeries.restrict_liftSeries_disjoint line 45
  9. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_liftSeries line 57
  10. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_identity line 73
  11. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_scalar line 78
  12. theorem OAI.FiniteEntropySeparation.FreeSeries.reparam_scalar_quadratic line 87
  13. theorem OAI.FiniteEntropySeparation.FreeSeries.Cyclic.append line 98
  14. theorem OAI.FiniteEntropySeparation.FreeSeries.cyclic_quadratic line 108
  15. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_moments line 117