OAI/Analysis/FreeEntropy/SeriesWeights.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.FreeSeries.truncEval line 9
  2. theorem OAI.FiniteEntropySeparation.FreeSeries.truncEval_nonneg line 10
  3. theorem OAI.FiniteEntropySeparation.FreeSeries.truncEval_mono line 12
  4. theorem OAI.FiniteEntropySeparation.FreeSeries.truncEval_le line 17
  5. theorem OAI.FiniteEntropySeparation.FreeSeries.truncEval_zero line 20
  6. theorem OAI.FiniteEntropySeparation.FreeSeries.truncEval_succ_shift line 21
  7. theorem OAI.FiniteEntropySeparation.FreeSeries.triangle_le_rectangle line 32
  8. def OAI.FiniteEntropySeparation.FreeSeries.scalarConv line 68
  9. theorem OAI.FiniteEntropySeparation.FreeSeries.truncEval_conv_le line 69
  10. theorem OAI.FiniteEntropySeparation.FreeSeries.substBound_trunc_le line 89
  11. def OAI.FiniteEntropySeparation.FreeSeries.seriesWeight line 121
  12. theorem OAI.FiniteEntropySeparation.FreeSeries.seriesWeight_nonneg line 122
  13. theorem OAI.FiniteEntropySeparation.FreeSeries.seriesWeight_conv_le line 124
  14. theorem OAI.FiniteEntropySeparation.FreeSeries.seriesWeight_subst_le line 128