OAI/NumberTheory/Catalan/Polynomial/ManuscriptLogCoefficientMass.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.ManuscriptPrecision.logCoefficientMass line 12
  2. def OAI.InternalCatalan.ManuscriptPrecision.tailCoefficientMass line 15
  3. def OAI.InternalCatalan.ManuscriptPrecision.pairLogCoefficients line 18
  4. def OAI.InternalCatalan.ManuscriptPrecision.normLogCoefficients line 21
  5. def OAI.InternalCatalan.ManuscriptPrecision.xLogCoefficients line 25
  6. def OAI.InternalCatalan.ManuscriptPrecision.yLogCoefficients line 30
  7. theorem OAI.InternalCatalan.ManuscriptPrecision.logCoefficientMass_nil line 34
  8. theorem OAI.InternalCatalan.ManuscriptPrecision.logCoefficientMass_cons line 36
  9. theorem OAI.InternalCatalan.ManuscriptPrecision.logCoefficientMass_append line 39
  10. theorem OAI.InternalCatalan.ManuscriptPrecision.logCoefficientMass_nonneg line 43
  11. theorem OAI.InternalCatalan.ManuscriptPrecision.tailCoefficientMass_nil line 50
  12. theorem OAI.InternalCatalan.ManuscriptPrecision.tailCoefficientMass_cons line 52
  13. theorem OAI.InternalCatalan.ManuscriptPrecision.tailCoefficientMass_nonneg line 55
  14. theorem OAI.InternalCatalan.ManuscriptPrecision.tailCoefficientMass_le_length line 58
  15. theorem OAI.InternalCatalan.ManuscriptPrecision.logCoefficientMass_scaled_tail line 69
  16. theorem OAI.InternalCatalan.ManuscriptPrecision.logCoefficientMass_neg_tail line 79
  17. theorem OAI.InternalCatalan.ManuscriptPrecision.logCoefficientMass_pair_lists line 87
  18. theorem OAI.InternalCatalan.ManuscriptPrecision.logCoefficientMass_pair line 97
  19. theorem OAI.InternalCatalan.ManuscriptPrecision.normLogCoefficients_mass line 103
  20. theorem OAI.InternalCatalan.ManuscriptPrecision.xLogCoefficients_mass line 110
  21. theorem OAI.InternalCatalan.ManuscriptPrecision.yLogCoefficients_mass line 122
  22. theorem OAI.InternalCatalan.ManuscriptPrecision.case2_tail_masses line 129
  23. theorem OAI.InternalCatalan.ManuscriptPrecision.case2_norm_mass_le line 139
  24. theorem OAI.InternalCatalan.ManuscriptPrecision.case2_X_mass_lt line 156
  25. theorem OAI.InternalCatalan.ManuscriptPrecision.case2_Y_mass_lt line 164
  26. theorem OAI.InternalCatalan.ManuscriptPrecision.case1_norm_mass_eq line 170
  27. theorem OAI.InternalCatalan.ManuscriptPrecision.case1_X_mass_eq line 174
  28. theorem OAI.InternalCatalan.ManuscriptPrecision.case1_X_mass_lt line 178
  29. theorem OAI.InternalCatalan.ManuscriptPrecision.case1_Y_mass_eq line 182
  30. theorem OAI.InternalCatalan.ManuscriptPrecision.case1_Y_mass_lt line 186