SequenceTilePacking.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A common separated-point bound for all probe tiles

The product lifts need not be unique. The proved lifted-cell packing inequality and common volume envelopes give one loss for every tile.

theorem OAI.PolycyclicRecognition.sequence_tile_separated_count line 24

Source documentation

The per-tile exponent survives passage from containing product regions to separated projected endpoints, uniformly over all tiles.

theorem sequence_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)
    (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 ≠ ⊤)
    (hE : ∀ n j, μ (E n j) ≠ ⊤) (hB : ∀ n, ν (B n) ≠ ⊤) {ρ : ℝ}
…