OAI/Analysis/FreeEntropy/SeriesNorm.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiniteEntropySeparation.FreeSeries.DegreeSpace line 12
  2. def OAI.FiniteEntropySeparation.FreeSeries.degreeVector line 13
  3. def OAI.FiniteEntropySeparation.FreeSeries.degreeNorm line 14
  4. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeVector_apply line 16
  5. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_nonneg line 18
  6. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_sq line 19
  7. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeVector_add line 22
  8. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeVector_smul line 24
  9. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_add_le line 26
  10. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_smul line 31
  11. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_zero line 36
  12. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_congr line 37
  13. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_le_of_coeff line 42
  14. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_sum_le line 47
  15. def OAI.FiniteEntropySeparation.FreeSeries.vectorSplit line 56
  16. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_tensor line 65
  17. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_conv_le line 78