OAI/Analysis/FreeEntropy/VectorSeries.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiniteEntropySeparation.FreeSeries.VSeries line 12
  2. abbrev OAI.FiniteEntropySeparation.FreeSeries.VDegreeSpace line 13
  3. def OAI.FiniteEntropySeparation.FreeSeries.vdegreeVector line 15
  4. def OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm line 17
  5. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeVector_apply line 18
  6. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_nonneg line 20
  7. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_sq line 21
  8. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_scalar line 24
  9. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_congr line 25
  10. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_zero_degree line 30
  11. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_add_le line 35
  12. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_zero line 39
  13. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_sum_le line 40
  14. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_tensor line 48
  15. def OAI.FiniteEntropySeparation.FreeSeries.vconv line 61
  16. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_conv_le line 63
  17. def OAI.FiniteEntropySeparation.FreeSeries.vsubst line 77
  18. theorem OAI.FiniteEntropySeparation.FreeSeries.vsubst_nil line 81
  19. theorem OAI.FiniteEntropySeparation.FreeSeries.vsubst_cons line 82
  20. theorem OAI.FiniteEntropySeparation.FreeSeries.vsubst_scalar line 84
  21. def OAI.FiniteEntropySeparation.FreeSeries.bundleDeriv line 97
  22. theorem OAI.FiniteEntropySeparation.FreeSeries.bundleDeriv_apply line 99
  23. def OAI.FiniteEntropySeparation.FreeSeries.vectorCons line 102
  24. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_bundleDeriv line 108
  25. theorem OAI.FiniteEntropySeparation.FreeSeries.vsubst_apply line 119
  26. theorem OAI.FiniteEntropySeparation.FreeSeries.vsubst_bundleDeriv line 134
  27. theorem OAI.FiniteEntropySeparation.FreeSeries.vdegreeNorm_subst_succ line 138
  28. def OAI.FiniteEntropySeparation.FreeSeries.substBound line 148
  29. theorem OAI.FiniteEntropySeparation.FreeSeries.substBound_nonneg line 153
  30. theorem OAI.FiniteEntropySeparation.FreeSeries.vsubst_norm_le line 163