OAI/Analysis/FreeEntropy/SeriesAnalytic.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_nil line 10
  2. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_unit_pos line 12
  3. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_neg line 18
  4. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_sub_unit_pos line 21
  5. theorem OAI.FiniteEntropySeparation.FreeSeries.seriesWeight_add_le line 28
  6. theorem OAI.FiniteEntropySeparation.FreeSeries.seriesWeight_neg line 36
  7. theorem OAI.FiniteEntropySeparation.FreeSeries.seriesWeight_agree line 38
  8. theorem OAI.FiniteEntropySeparation.FreeSeries.seriesWeight_split line 45
  9. theorem OAI.FiniteEntropySeparation.FreeSeries.seriesWeight_unit line 52
  10. theorem OAI.FiniteEntropySeparation.FreeSeries.inverse_tail_identity line 56
  11. theorem OAI.FiniteEntropySeparation.FreeSeries.inverse_tail_weight line 61
  12. theorem OAI.FiniteEntropySeparation.FreeSeries.seriesWeight_coeff_le line 76
  13. theorem OAI.FiniteEntropySeparation.FreeSeries.degreeNorm_le_of_weight line 80
  14. theorem OAI.FiniteEntropySeparation.FreeSeries.seriesWeight_mono_radius line 87
  15. theorem OAI.FiniteEntropySeparation.FreeSeries.geom_tail_le line 93
  16. theorem OAI.FiniteEntropySeparation.FreeSeries.weight_le_geom line 99
  17. theorem OAI.FiniteEntropySeparation.FreeSeries.subst_weight_le line 113
  18. theorem OAI.FiniteEntropySeparation.FreeSeries.moments_tail_weight line 117