OAI/Analysis/LipschitzHilbert/Estimates/TileLatticeEnvelope.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform overlap for actual rectangular tile-center lattices, allowing arbitrary horizontal and vertical scales and finite subfamilies.

  1. theorem OAI.LipschitzHilbert.finite_scaled_plane_lattice_overlap line 13
  2. theorem OAI.LipschitzHilbert.injective_tile_lattice_overlap line 29