OAI/Combinatorics/Progressions/Lattices/ResidueBoxSliceCoordinateDisintegration.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.ResidueBoxSlice.integerPoint line 15
  2. theorem OAI.Erdos3.ResidueBoxSlice.integerPoint_eq line 18
  3. theorem OAI.Erdos3.ResidueBoxSlice.commonStrideIndex_integerPoint line 24
  4. theorem OAI.Erdos3.ResidueBoxSlice.integerPoint_injective line 30
  5. def OAI.Erdos3.ResidueBoxSlice.integerPoints line 41
  6. theorem OAI.Erdos3.ResidueBoxSlice.integerPoints_eq_commonStrideBox line 44
  7. theorem OAI.Erdos3.ResidueBoxSlice.progression_inside line 67
  8. theorem OAI.Erdos3.ResidueBoxSlice.isDenseCommonStrideBox line 81
  9. theorem OAI.Erdos3.ResidueBoxSlice.densityCost_nonneg line 93
  10. theorem OAI.Erdos3.ResidueBoxSlice.expect_integerPoints line 100
  11. theorem OAI.Erdos3.IsDenseCommonStrideBox.mono line 110
  12. theorem OAI.Erdos3.commonStrideBox_axis_card line 130
  13. theorem OAI.Erdos3.ResidueBoxSlice.length_pos_of_integerPoints_nonempty line 146
  14. theorem OAI.Erdos3.ResidueBoxSlice.length_pos_of_dense line 153
  15. theorem OAI.Erdos3.ResidueBoxSlice.length_lower_of_dense line 158
  16. def OAI.Erdos3.ResidueBoxSlice.enlargeBox line 186
  17. theorem OAI.Erdos3.ResidueBoxSlice.enlargeBox_start line 192
  18. theorem OAI.Erdos3.ResidueBoxSlice.enlargeBox_length line 195
  19. theorem OAI.Erdos3.ResidueBoxSlice.enlargeBox_integerPoint line 198
  20. theorem OAI.Erdos3.ResidueBoxSlice.enlargeBox_integerPoints line 204
  21. theorem OAI.Erdos3.ResidueBoxSlice.expect_enlargeBox line 208
  22. def OAI.Erdos3.integerBoxInclusion line 218
  23. theorem OAI.Erdos3.integerBoxInclusion_val line 224
  24. theorem OAI.Erdos3.IsDenseCommonStrideBox.enlargeBox line 227
  25. theorem OAI.Erdos3.ResidueBoxSlice.enlargeBox_dense line 247
  26. theorem OAI.Erdos3.ResidueBoxSlice.enlargeBox_length_lower line 255
  27. theorem OAI.Erdos3.ResidueBoxSlice.enlargeBox_fullSlicePointInIntegerBox line 268
  28. theorem OAI.Erdos3.ResidueBoxSlice.enlargeBox_fullSliceLaw_mean line 273
  29. theorem OAI.Erdos3.ResidueBoxSlice.enlargeBox_fullSliceLaw_mean_ambient line 281
  30. theorem OAI.Erdos3.ResidueBoxSlice.enlargeBox_fullSliceLaw line 288
  31. theorem OAI.Erdos3.RelativePatchSliceConclusion.enlargeBox line 310
  32. def OAI.Erdos3.ResidueBoxSlice.finiteSites line 335
  33. theorem OAI.Erdos3.ResidueBoxSlice.finiteSites_image_integerCast line 338
  34. theorem OAI.Erdos3.ResidueBoxSlice.finiteBox_integerCast_injective line 346
  35. theorem OAI.Erdos3.ResidueBoxSlice.expect_finiteSites line 353
  36. theorem OAI.Erdos3.ResidueBoxSlice.finiteSites_nonempty line 361
  37. theorem OAI.Erdos3.ResidueBoxSlice.finiteSites_nonempty_of_integerPoints line 367
  38. theorem OAI.Erdos3.ResidueBoxSlice.finiteSites_dense line 373
  39. def OAI.Erdos3.ResidueBoxSlice.comap line 393
  40. def OAI.Erdos3.ResidueBoxSlice.coordinateProjection line 399
  41. theorem OAI.Erdos3.ResidueBoxSlice.comap_isDenseCommonStrideBox line 405
  42. theorem OAI.Erdos3.ResidueBoxSlice.coordinateProjection_isDenseCommonStrideBox line 417
  43. theorem OAI.Erdos3.ResidueBoxSlice.mem_integerPoints_iff line 424
  44. theorem OAI.Erdos3.ResidueBoxSlice.finiteSplitPoint_mem_integerPoints line 430
  45. theorem OAI.Erdos3.ResidueBoxSlice.exists_coordinate_fiber_score line 444
  46. def OAI.Erdos3.ResidueBoxSlice.axisInclusion line 503
  47. def OAI.Erdos3.ResidueBoxSlice.axisInsertion line 507
  48. theorem OAI.Erdos3.ResidueBoxSlice.axisInsertion_kept line 512
  49. theorem OAI.Erdos3.ResidueBoxSlice.axisInsertion_injective line 518
  50. def OAI.Erdos3.ResidueBoxSlice.extendAxes line 528
  51. theorem OAI.Erdos3.ResidueBoxSlice.extendAxes_integerPoints line 551
  52. theorem OAI.Erdos3.ResidueBoxSlice.expect_extendAxes line 597
  53. theorem OAI.Erdos3.ResidueBoxSlice.extendAxes_dense line 611
  54. theorem OAI.Erdos3.ResidueBoxSlice.extendAxes_subset line 649
  55. theorem OAI.Erdos3.ResidueBoxSlice.coordinate_complexMean line 681
  56. theorem OAI.Erdos3.ResidueBoxSlice.exists_coordinate_fiber_norm line 718
  57. theorem OAI.Erdos3.ResidueBoxSlice.exists_coordinate_fiber_correlation line 747