RetainedProbeAnchors.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Retaining the good anchors needed by measured packing

def OAI.PolycyclicRecognition.occupiedTileAnchor line 16
Source documentation
Empty image tiles use the original neighboring sheet as anchor. An occupied tile retains its exact geometric anchor.
```
def occupiedTileAnchor {G X : Type*} {m : ℕ}
    (points : Fin m → Finset X) (anchor : Fin m → G) (fallback : G) (j : Fin m) : G :=
…
```
theorem OAI.PolycyclicRecognition.occupiedTileAnchor_eq line 20

theorem OAI.PolycyclicRecognition.occupiedTileAnchor_profile_bound line 29

Source documentation

The simultaneous good-probe estimate extends to every tile after replacing empty tiles. This supplies the all-anchor premise of packing without requiring unselected anchors to have good profiles.

theorem occupiedTileAnchor_profile_bound
    {G X W : Type*} [NormedAddCommGroup W]
    {Y : ℕ → Type*} (good : ∀ n, Set (Y n)) (tiles : ℕ → ℕ)
    (tile : ∀ n, Y n → Fin (tiles n))
    (points : ∀ n, Fin (tiles n) → Finset X)
    (anchor : ∀ n, Fin (tiles n) → G) (fallback : ℕ → G)
    (profile : ℕ → G → W) (target : ℕ → W) (ε : ℕ → ℝ)
    (hwitness : ∀ n j x, x ∈ points n j → ∃ y ∈ good n, tile n y = j)
    (hfallback : ∀ᶠ n in atTop, ‖profile n (fallback n) - target n‖ ≤ ε n)
    (hgood : ∀ᶠ n in atTop, ∀ y ∈ good n,
      ‖profile n (anchor n (tile n y)) - target n‖ ≤ ε n) :
    ∀ᶠ n in atTop, ∀ j,
…