OAI/Geometry/PeriodicTiling/Activation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.MixedDifferenceZero line 22
  2. theorem OAI.PeriodicTilingThree.zmod_eq_zero_of_pred_invariant line 25
  3. theorem OAI.PeriodicTilingThree.mixedDifference_rectangle line 39
  4. theorem OAI.PeriodicTilingThree.histogram_separable line 59
  5. theorem OAI.PeriodicTilingThree.histogram_mass_eq line 76
  6. theorem OAI.PeriodicTilingThree.histogram_mass_dvd line 91
  7. theorem OAI.PeriodicTilingThree.sum_histogram_corner line 108
  8. theorem OAI.PeriodicTilingThree.sum_shiftOmega_mul line 123
  9. theorem OAI.PeriodicTilingThree.mixedDifferenceZero_of_shift_sum line 144
  10. theorem OAI.PeriodicTilingThree.histogram_mass_dvd_of_shift_sum line 169
  11. theorem OAI.PeriodicTilingThree.sum_firstCoordinate_of_bijective line 177
  12. theorem OAI.PeriodicTilingThree.card_firstCoordinate_of_bijective line 190
  13. theorem OAI.PeriodicTilingThree.sum_firstFirstCoordinate_of_bijective line 197
  14. theorem OAI.PeriodicTilingThree.card_firstFirstCoordinate_of_bijective line 210
  15. def OAI.PeriodicTilingThree.seedHistogram line 219
  16. theorem OAI.PeriodicTilingThree.seedHistogram_eq_sum line 224
  17. theorem OAI.PeriodicTilingThree.sum_seedHistogram line 229
  18. theorem OAI.PeriodicTilingThree.sum_seedHistogram_translate line 241
  19. theorem OAI.PeriodicTilingThree.ordinary_active_of_tile line 254
  20. theorem OAI.PeriodicTilingThree.seed_active_somewhere_of_tile line 298