OAI/GroupTheory/PolycyclicRecognition/Analysis/TiledProbeSamplers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_measurable_tiled_probe_samplers line 24

   Source documentation

   A finite measurable tiling supplies the actual first-sheet, reverse-anchor, and within-tile samplers. Their group increments are the original endpoints, so choosing a tile never replaces a counted point by another representative.

   theorem exists_measurable_tiled_probe_samplers
       (ι : I →* N) (hι : Measurable ι) (φ : I ≃ₜ* I) (k : N)
       (hφ : ∀ z, ι (φ z) = k * ι z * k⁻¹)
       (σ : Z → N) (hσ : Measurable σ)
       (U Banchor Bsmall : Set I) {m : ℕ} (anchor : Fin m → I)
       (tile : Fin m → Set I) (hm : ∀ j, MeasurableSet (tile j))
       (hd : Pairwise (fun j l => Disjoint (tile j) (tile l)))
       (hu : (⋃ j, tile j) = U)
       (ha : ∀ j, φ.symm (anchor j) ∈ Banchor)
       (ht : ∀ j, tile j ⊆ anchor j • (φ '' Bsmall)) :
       ∃ (index : U → Fin m) (probe : Fin 3 → Z × U → N),
         Measurable index ∧ (∀ j, Measurable (probe j)) ∧
   …