SnappedLattice.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Put translated sheared packet lattices on a common reference lattice. The site map is injective and moves each center by at most one mesh in both coordinates. No equality of the physical and reference lattices is assumed.

def OAI.LipschitzHilbert.snappedLatticeSite line 15
Source documentation
Quantize a translated, sheared lattice without identifying distinct sites of that lattice. The shear is measured in the reference coordinates.
```
def snappedLatticeSite (a b l W delta : ℝ) (q : ℤ × ℤ) : ℤ × ℤ :=
…
```
theorem OAI.LipschitzHilbert.snappedLatticeSite_injective line 18
theorem OAI.LipschitzHilbert.floor_mesh_error line 29
theorem OAI.LipschitzHilbert.snappedLatticeSite_horizontal line 38
theorem OAI.LipschitzHilbert.snappedLatticeSite_vertical line 46
theorem OAI.LipschitzHilbert.lineEnvelope_near_center line 55
Source documentation
Moving a center by at most one mesh preserves any fixed decay order.
```
theorem lineEnvelope_near_center (a b l x : ℝ) (n : ℕ) (hl : 0 < l)
    (hab : |a-b| ≤ l) :
    lineEnvelope a l n x ≤ 3^n*lineEnvelope b l n x := by
…
```
Mentions: OAI.LipschitzHilbert.lineEnvelope

theorem OAI.LipschitzHilbert.snappedLatticeSite_envelope line 79

Source documentation

Product decay survives the actual center quantization with fixed cost.

theorem snappedLatticeSite_envelope (a b l W delta x y : ℝ)
    (hl : 0 < l) (hW : 0 < W) (q : ℤ × ℤ) (nx ny : ℕ) :
    lineEnvelope (a+l*q.1) l nx x *
        lineEnvelope (b+delta*l*q.1+W*q.2) W ny y ≤
      (3^nx*3^ny) *
        (lineEnvelope (l*(snappedLatticeSite a b l W delta q).1) l nx x *
          lineEnvelope (W*(snappedLatticeSite a b l W delta q).2) W ny y) := by
…

Mentions: OAI.LipschitzHilbert.lineEnvelope, OAI.LipschitzHilbert.snappedLatticeSite