AnchoredTilePacking.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Packing tiles whose factor lifts use different anchors

Endpoint sets stay in the common ambient frame. Each tile may choose its own left-translated factor coordinates without changing its cardinality or the separation constant.

theorem OAI.PolycyclicRecognition.factor_anchored_card_le_product_volume line 22

theorem OAI.PolycyclicRecognition.sequence_anchored_tile_separated_count line 62

Source documentation

Common per-tile bounds in independently translated factor frames.

theorem sequence_anchored_tile_separated_count
    (φ : D →* MulAut N) (ι : N →* G) (κ : D →* G)
    (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (μ : Measure N) (ν : Measure D) [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
    [SFinite μ] [SFinite ν] (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
    (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
    (tiles : ℕ → ℕ) (s : ∀ n, Fin (tiles n) → Finset G)
    (anchor : ∀ n, Fin (tiles n) → G)
    (p : ∀ n, Fin (tiles n) → G → N × D)
    (E : ∀ n, Fin (tiles n) → Set N) (B : ℕ → Set D)
    (U : Set (N × D)) (hU : MeasurableSet U)
    (hU0 : (μ.prod ν) U ≠ 0) (hUtop : (μ.prod ν) U ≠ ⊤)
…