OAI/Combinatorics/Progressions/Linear/MahlerBasis.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.IntegerBasisReduction.Mahler.IntegralPoint line 13
  2. def OAI.Erdos3.IntegerBasisReduction.Mahler.integralEmbed line 15
  3. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.integralEmbed_zero line 19
  4. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.integralEmbed_add line 25
  5. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.integralEmbed_zsmul line 31
  6. def OAI.Erdos3.IntegerBasisReduction.Mahler.AdmitsIndependent line 36
  7. def OAI.Erdos3.IntegerBasisReduction.Mahler.successiveMinimum line 42
  8. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.AdmitsIndependent.mono line 46
  9. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.AdmitsIndependent.nonneg line 53
  10. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.successiveMinimum_nonneg line 59
  11. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.successiveMinimum_le_of_admits line 66
  12. def OAI.Erdos3.IntegerBasisReduction.Mahler.mahlerFactor line 74
  13. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.mahlerFactor_zero line 78
  14. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.mahlerFactor_of_pos line 82
  15. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.mahlerFactor_nonneg line 86
  16. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.mahlerFactor_le_rank line 94
  17. def OAI.Erdos3.IntegerBasisReduction.Mahler.IsDefinite line 104
  18. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.isDefinite_gaugeSeminorm line 107
  19. def OAI.Erdos3.IntegerBasisReduction.Mahler.IsMahlerBasis line 114
  20. def OAI.Erdos3.IntegerBasisReduction.Mahler.MahlerBasisStatement line 119
  21. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.exists_isMahlerBasis_zero line 124
  22. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.exists_isMahlerBasis_one line 130
  23. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.IsMahlerBasis.first line 191
  24. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.IsMahlerBasis.later line 197
  25. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.IsMahlerBasis.le_rank_mul_successiveMinimum line 204
  26. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.seminorm_sum_le line 212
  27. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.seminorm_sum_basis_le line 225
  28. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.seminorm_sum_integralBasis_le line 235
  29. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.IsMahlerBasis.seminorm_sum_le line 243