OAI/Combinatorics/Progressions/Sampling/RationalSpanGrid.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.IntegralVector line 23
  2. theorem OAI.Erdos3.IntegralVector.nat_smul line 25
  3. def OAI.Erdos3.scaledIntegerGrid line 31
  4. def OAI.Erdos3.denominatorGrid line 34
  5. theorem OAI.Erdos3.mem_denominatorGrid_iff line 37
  6. def OAI.Erdos3.matrixDenominator line 52
  7. def OAI.Erdos3.clearedMatrix line 55
  8. theorem OAI.Erdos3.matrixDenominator_pos line 59
  9. theorem OAI.Erdos3.matrixDenominator_le line 63
  10. theorem OAI.Erdos3.clearedMatrix_cast line 69
  11. theorem OAI.Erdos3.integralVector_denominator_mulVec line 74
  12. theorem OAI.Erdos3.exists_bounded_rational_left_inverse line 83
  13. theorem OAI.Erdos3.rational_embedding_grid_bounds line 95
  14. theorem OAI.Erdos3.exists_bounded_subspace_grid line 111
  15. def OAI.Erdos3.integerGridImage line 125
  16. theorem OAI.Erdos3.rational_quotient_grid_bounds line 128
  17. theorem OAI.Erdos3.exists_bounded_quotient_grid line 144
  18. theorem OAI.Erdos3.rational_grid_height_le_exp line 165
  19. theorem OAI.Erdos3.exists_subspace_grid_exp_bound line 194
  20. theorem OAI.Erdos3.exists_quotient_grid_exp_bound line 210
  21. theorem OAI.Erdos3.finite_card_rational_grid_box line 235
  22. theorem OAI.Erdos3.scaledIntegerGrid_subset_of_dvd line 276
  23. theorem OAI.Erdos3.denominatorGrid_subset_of_dvd line 285
  24. def OAI.Erdos3.realIntegerGrid line 305
  25. def OAI.Erdos3.realDenominatorGrid line 307
  26. theorem OAI.Erdos3.isClosedEmbedding_integerVectors line 310
  27. theorem OAI.Erdos3.isClosed_realIntegerGrid line 314
  28. theorem OAI.Erdos3.isClosed_realDenominatorGrid line 317
  29. theorem OAI.Erdos3.real_cast_mem_denominatorGrid_iff line 321
  30. theorem OAI.Erdos3.isDiscrete_realIntegerGrid line 339
  31. theorem OAI.Erdos3.isDiscrete_realDenominatorGrid line 342
  32. theorem OAI.Erdos3.closed_discrete_of_real_grid line 347
  33. theorem OAI.Erdos3.scaled_grid_mulVec line 365
  34. theorem OAI.Erdos3.rational_preimage_grid_transport line 370
  35. theorem OAI.Erdos3.rational_image_grid_transport line 390
  36. theorem OAI.Erdos3.grid_allowance_mul_le_exp line 408
  37. theorem OAI.Erdos3.exists_preimage_grid_exp_bound line 425
  38. theorem OAI.Erdos3.exists_image_grid_exp_bound line 446
  39. theorem OAI.Erdos3.grid_box_count_le_exp line 479
  40. theorem OAI.Erdos3.finite_index_of_bounded_grid_representatives line 537
  41. theorem OAI.Erdos3.grid_det_integer_multiple line 579
  42. theorem OAI.Erdos3.one_div_pow_le_abs_grid_det line 592
  43. theorem OAI.Erdos3.realDenominatorGrid_nat_smul_iff line 614
  44. theorem OAI.Erdos3.linearMap_grid_of_integer line 619
  45. def OAI.Erdos3.spanningCoordinateMatrix line 644
  46. theorem OAI.Erdos3.spanningCoordinateMatrix_mulVec line 647
  47. def OAI.Erdos3.rationalSpanGridStep line 652
  48. theorem OAI.Erdos3.rationalSpanGridStep_pos line 655
  49. theorem OAI.Erdos3.rationalSpanGridStep_le line 659
  50. theorem OAI.Erdos3.rationalSpanGridStep_combination line 664