OAI/Geometry/PeriodicTiling/DirectionalLimits.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.directionalAverage line 28
  2. theorem OAI.PeriodicTilingThree.directionalAverage_nonneg line 31
  3. theorem OAI.PeriodicTilingThree.directionalAverage_le_one line 37
  4. theorem OAI.PeriodicTilingThree.directionalAverage_translate_sub line 47
  5. theorem OAI.PeriodicTilingThree.directionalAverage_translate_error line 63
  6. theorem OAI.PeriodicTilingThree.sum_directionalAverage line 75
  7. theorem OAI.PeriodicTilingThree.exists_common_directional_subsequence line 93
  8. theorem OAI.PeriodicTilingThree.exists_ungrouped_directional_limits line 108
  9. theorem OAI.PeriodicTilingThree.Tiles.exists_ungrouped_directional_limits line 146
  10. theorem OAI.PeriodicTilingThree.exists_grouped_directional_functions line 156
  11. theorem OAI.PeriodicTilingThree.Tiles.exists_directional_decomposition line 251