OAI/GroupTheory/PolycyclicRecognition/Analysis/FiniteTranslateCover.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.disjoint_translate_card_mul_le line 17
2. theorem OAI.PolycyclicRecognition.exists_finite_translate_cover line 32

   Source documentation

   A finite maximal disjoint family exists because every such family has cardinality bounded by the containing region's volume. Its doubled tiles cover every allowed anchor.

   theorem exists_finite_translate_cover (μ : Measure G) [μ.IsMulLeftInvariant]
       (S Q R : Set G) (hQ : MeasurableSet Q)
       (hQ0 : μ Q ≠ 0) (hQtop : μ Q ≠ ⊤) (hRtop : μ R ≠ ⊤)
       (hcontain : ∀ a ∈ S, a • Q ⊆ R) :
       ∃ t : Finset G, (t : Set G) ⊆ S ∧
         (t : Set G).PairwiseDisjoint (fun a => a • Q) ∧
         (t.card : ℝ≥0∞) * μ Q ≤ μ R ∧
         S ⊆ ⋃ a ∈ t, a • (Q * Q⁻¹) := by
   …

3. theorem OAI.PolycyclicRecognition.measurable_partition_of_finite_cover line 100