OAI/GroupTheory/PolycyclicRecognition/Analysis/FiniteConjugateTiling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.finite_conjugate_tiling line 20

   Source documentation

   A measure-preserving group automorphism can distort tiles without altering the cardinality bound. The doubled small box suffices for a measurable partition of the large box.

   theorem finite_conjugate_tiling (μ : Measure G) [μ.IsMulLeftInvariant]
       (e : G ≃ₜ* G) (he : MeasurePreserving e μ μ)
       (S B Bplus R : Set G) (hS : MeasurableSet S)
       (hB : IsCompact B) (hBplus : IsCompact Bplus)
       (hB0 : μ B ≠ 0) (hBtop : μ B ≠ ⊤) (hRtop : μ R ≠ ⊤)
       (hcontain : S * (e '' B) ⊆ R) (hdouble : B * B⁻¹ ⊆ Bplus) :
       ∃ (n : ℕ) (anchor : Fin n → G) (tile : Fin n → Set G),
         (∀ i, anchor i ∈ S) ∧
         (∀ i, MeasurableSet (tile i)) ∧
         Pairwise (fun i j => Disjoint (tile i) (tile j)) ∧
         (⋃ i, tile i) = S ∧
         (∀ i, tile i ⊆ anchor i • (e '' Bplus)) ∧
   …