OAI/Analysis/FreeEntropy/SemicircularSeries.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.FreeSeries.letter line 10
  2. def OAI.FiniteEntropySeparation.FreeSeries.quadratic line 13
  3. theorem OAI.FiniteEntropySeparation.FreeSeries.letter_nil line 16
  4. theorem OAI.FiniteEntropySeparation.FreeSeries.quadratic_nil line 17
  5. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_letter line 18
  6. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_letter_cons line 23
  7. theorem OAI.FiniteEntropySeparation.FreeSeries.deriv_quadratic line 27
  8. theorem OAI.FiniteEntropySeparation.FreeSeries.quadratic_subst_derivative line 33
  9. def OAI.FiniteEntropySeparation.FreeSeries.fockMoments line 44
  10. theorem OAI.FiniteEntropySeparation.FreeSeries.fockMoments_eq line 45
  11. theorem OAI.FiniteEntropySeparation.FreeSeries.fockMoments_moments line 52
  12. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_succ_sq line 56
  13. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_letter_one line 65
  14. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_quadratic_sq line 75
  15. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_quadratic_other line 78
  16. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_quadratic line 91
  17. theorem OAI.FiniteEntropySeparation.FreeSeries.quadratic_weight_le line 94
  18. theorem OAI.FiniteEntropySeparation.FreeSeries.fockMoments_norm_le line 106