OAI/Combinatorics/Progressions/Lattices/PhysicalSubboxResidueSlice.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerBox line 18
  2. theorem OAI.Erdos3.mem_integerBox line 21
  3. abbrev OAI.Erdos3.BoxAmbient line 25
  4. def OAI.Erdos3.boxReduction line 27
  5. theorem OAI.Erdos3.boxReduction_apply line 33
  6. theorem OAI.Erdos3.int_eq_of_zmod_eq_of_bounds line 37
  7. theorem OAI.Erdos3.boxReduction_reflectsPairSums line 43
  8. theorem OAI.Erdos3.boxReduction_injOn line 62
  9. def OAI.Erdos3.integerBoxCubeEquiv line 66
  10. theorem OAI.Erdos3.integerBox_expect_eq_zmod line 81
  11. theorem OAI.Erdos3.integerBox_subtype_mean_eq_fin line 111
  12. def OAI.Erdos3.integerCyclicMap line 149
  13. theorem OAI.Erdos3.integerInterval_reflectsPairSums line 151
  14. theorem OAI.Erdos3.integerInterval_image_cyclicInterval line 168
  15. def OAI.Erdos3.integerBoxCubeCount line 203
  16. def OAI.Erdos3.integerBoxGowersNorm line 206
  17. theorem OAI.Erdos3.integerBox_nonempty line 211
  18. theorem OAI.Erdos3.integerBoxCubeCount_eq_groupCubeCount line 217
  19. theorem OAI.Erdos3.integerBoxCubeCount_pos line 221
  20. theorem OAI.Erdos3.integerBoxGowersNorm_one line 225
  21. theorem OAI.Erdos3.integerBoxGowersNorm_eq_restricted line 229
  22. theorem OAI.Erdos3.integerBoxGowersNorm_ambient_comparison line 235
  23. theorem OAI.Erdos3.integerBoxGowersNorm_add line 241
  24. theorem OAI.Erdos3.integerBoxGowersNorm_degree_one line 246
  25. theorem OAI.Erdos3.integerBoxGowersNorm_pow_tsum line 251
  26. theorem OAI.Erdos3.integerBox_mixed_cauchy_schwarz line 261
  27. theorem OAI.Erdos3.card_integerBox line 280
  28. def OAI.Erdos3.smallCubeSide line 283
  29. theorem OAI.Erdos3.small_increments_supported line 287
  30. def OAI.Erdos3.smallBoxCubeMap line 327
  31. theorem OAI.Erdos3.smallBoxCubeMap_injective line 334
  32. theorem OAI.Erdos3.small_box_card_pow_le_cubeCount line 343
  33. theorem OAI.Erdos3.card_integerBox_le_small_box line 351
  34. theorem OAI.Erdos3.integerBoxCubeCount_lower line 365
  35. theorem OAI.Erdos3.integerBoxCubeCount_upper line 373
  36. theorem OAI.Erdos3.integerBoxCubeCount_bounds line 377
  37. def OAI.Erdos3.integerBoxTestExtension line 406
  38. theorem OAI.Erdos3.integerBoxTestExtension_integer line 410
  39. theorem OAI.Erdos3.integerBoxTestExtension_norm_le_one line 423
  40. theorem OAI.Erdos3.integerBoxTestExtension_of_mem line 431
  41. theorem OAI.Erdos3.integerBoxTestExtension_of_not_mem line 436
  42. def OAI.Erdos3.translatedIntegerBox line 453
  43. theorem OAI.Erdos3.mem_translatedIntegerBox line 456
  44. theorem OAI.Erdos3.translatedIntegerBox_nonempty line 466
  45. theorem OAI.Erdos3.translatedIntegerBox_reflectsPairSums line 470
  46. theorem OAI.Erdos3.translatedIntegerBox_norm_eq line 475
  47. theorem OAI.Erdos3.translatedIntegerBox_norm_degree_one line 480
  48. theorem OAI.Erdos3.translatedIntegerBox_cubeCount_bounds line 486
  49. theorem OAI.Erdos3.integerBox_weighted_derivative line 495
  50. theorem OAI.Erdos3.integerBox_sum_derivative_weights line 506
  51. def OAI.Erdos3.trimmedIntegerBox line 524
  52. theorem OAI.Erdos3.card_trimmedIntegerBox line 527
  53. theorem OAI.Erdos3.trimmedIntegerBox_nonempty line 532
  54. theorem OAI.Erdos3.trimmedIntegerBox_add_mem line 540
  55. theorem OAI.Erdos3.trimmedIntegerBox_card_deficit line 552
  56. theorem OAI.Erdos3.derivativeSupport_translatedIntegerBox line 585
  57. theorem OAI.Erdos3.box_overlap_length_pos line 599
  58. theorem OAI.Erdos3.box_differenceSupport_subset line 613
  59. theorem OAI.Erdos3.card_box_differenceSupport_le line 626
  60. def OAI.Erdos3.translatedIntegerBoxEquivPi line 643
  61. theorem OAI.Erdos3.translatedIntegerBoxEquivPi_val line 651
  62. def OAI.Erdos3.integerResidueBoxEquiv line 655
  63. theorem OAI.Erdos3.integerResidueBoxEquiv_val line 662
  64. theorem OAI.Erdos3.integerResidueBox_expect line 668
  65. theorem OAI.Erdos3.integerResidueBox_lengths_pos line 684
  66. def OAI.Erdos3.physicalResidueCoordinateEquiv line 700
  67. theorem OAI.Erdos3.physicalResidueCoordinateEquiv_val line 708
  68. theorem OAI.Erdos3.ResidueBoxSlice.physicalResidue_start_nonneg line 721
  69. def OAI.Erdos3.ResidueBoxSlice.ofPhysicalResidue line 730
  70. theorem OAI.Erdos3.ResidueBoxSlice.ofPhysicalResidue_length line 746
  71. theorem OAI.Erdos3.ResidueBoxSlice.ofPhysicalResidue_start line 750
  72. theorem OAI.Erdos3.ResidueBoxSlice.ofPhysicalResidue_length_pos line 754
  73. theorem OAI.Erdos3.ResidueBoxSlice.ofPhysicalResidue_point_int line 757
  74. def OAI.Erdos3.ResidueBoxSlice.ofPhysicalResidueEquiv line 766
  75. theorem OAI.Erdos3.ResidueBoxSlice.ofPhysicalResidueEquiv_val line 772