OAI/Combinatorics/Progressions/Linear/ProperCyclicKernelBasis.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.IntegerBasisReduction.Mahler.IsSeminormOrdered line 20
  2. def OAI.Erdos3.IntegerBasisReduction.Mahler.basisReductionStandardPoint line 25
  3. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.integralEmbed_basisReductionStandardPoint line 30
  4. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.linearIndependent_basisReductionStandardPoint line 39
  5. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.AdmitsIndependent.antitone_rank_basisReduction line 45
  6. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.successiveMinimum_set_nonempty_basisReduction line 52
  7. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.successiveMinimum_mono_basisReduction line 67
  8. def OAI.Erdos3.IntegerBasisReduction.Mahler.IsCenteredReduction line 78
  9. def OAI.Erdos3.IntegerBasisReduction.Mahler.IsRawFlagReduction line 88
  10. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.exists_rawFlagReduction_of_linearIndependent line 98
  11. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.rawFlagReduction_diag_abs_le_one line 184
  12. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.rawFlagReduction_diag_abs_le_half_of_not_unit line 201
  13. def OAI.Erdos3.IntegerBasisReduction.Mahler.prefixIndex line 219
  14. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.prefixIndex_val line 222
  15. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.prefixIndex_injective line 225
  16. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.prefixIndex_lt line 231
  17. def OAI.Erdos3.IntegerBasisReduction.Mahler.centeredStep line 234
  18. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.abs_centeredStep_apply_self_le line 238
  19. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.centeredStep_apply_of_eq_zero line 254
  20. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.exists_integerCombination_abs_le_half line 259
  21. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.exists_prefix_integerCombination_abs_le_half line 306
  22. def OAI.Erdos3.IntegerBasisReduction.Mahler.shearMatrix line 326
  23. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.shearMatrix_isUpperTriangular line 330
  24. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.shearMatrix_apply_self line 339
  25. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.shearMatrix_det line 345
  26. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.shearMatrix_isUnit_det line 351
  27. def OAI.Erdos3.IntegerBasisReduction.Mahler.shearBasis line 357
  28. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.shearBasis_apply line 363
  29. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.shearBasis_apply_eq_add_Iio line 369
  30. def OAI.Erdos3.IntegerBasisReduction.Mahler.basisOfUpperTriangularUnits line 402
  31. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.basisOfUpperTriangularUnits_apply line 412
  32. def OAI.Erdos3.IntegerBasisReduction.Mahler.extendPrefix line 421
  33. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.extendPrefix_prefixIndex line 425
  34. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.extendPrefix_eq_zero_of_not_lt line 430
  35. def OAI.Erdos3.IntegerBasisReduction.Mahler.prefixIndexEquivIio line 435
  36. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.sum_extendPrefix_mul line 446
  37. def OAI.Erdos3.IntegerBasisReduction.Mahler.centeredReductionMatrix line 469
  38. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.centeredReductionMatrix_isUpperTriangular line 478
  39. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.centeredReductionMatrix_apply_self line 494
  40. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.centeredReductionMatrix_isUnit_diagonal line 511
  41. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.exists_centeredReduction_of_rawFlagReduction line 520
  42. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.exists_centeredReduction_of_linearIndependent line 661
  43. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.centeredReduction_sum_eq_single line 669
  44. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.seminorm_basis_le_of_primitive_branch line 684
  45. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.seminorm_basis_le_half_sum line 698
  46. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.seminorm_basis_le_max_of_centeredReduction line 734
  47. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.seminorm_basis_le_of_centered_branch line 750
  48. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.seminorm_basis_le_mahlerFactor_mul line 775
  49. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.isMahlerBasis_of_centeredReduction line 814
  50. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.isMahlerBasis_of_centeredReduction_of_minima_upper line 827
  51. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.exists_isMahlerBasis_of_centeredReduction_of_minima_upper line 872
  52. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.exists_isMahlerBasis_of_linearIndependent_of_minima_upper line 883
  53. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.exists_isMahlerBasis_of_centeredReduction line 892
  54. theorem OAI.Erdos3.IntegerBasisReduction.Mahler.IsCenteredReduction.abs_coefficient_le_one line 914
  55. theorem OAI.Erdos3.exists_lattice_basis_bounded_expansion line 929
  56. theorem OAI.Erdos3.exists_lattice_basis_coordinate_bound line 966
  57. theorem OAI.Erdos3.cyclicIntegerKernel_eq_zero_of_lt_radii line 1000
  58. theorem OAI.Erdos3.cyclicIntegerKernel_nonzero_large_coordinate line 1014
  59. theorem OAI.Erdos3.affine_box_card_le_radius_product line 1022
  60. theorem OAI.Erdos3.cyclicIntegerKernel_normalized_covolume_le line 1042
  61. theorem OAI.Erdos3.exists_short_independent_cyclic_kernel_vectors line 1055
  62. theorem OAI.Erdos3.proper_cyclic_kernel_box_card_le_covolume line 1120
  63. theorem OAI.Erdos3.proper_cyclic_kernel_covolume_lower_bound line 1139
  64. def OAI.Erdos3.properCyclicKernelBasisBound line 1151
  65. theorem OAI.Erdos3.properCyclicKernelBasisBound_nonneg line 1154
  66. theorem OAI.Erdos3.exists_proper_cyclic_kernel_basis line 1159
  67. theorem OAI.Erdos3.exists_proper_affine_torus_basis line 1179