OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactTupleThickening.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_small_factor_tuple_neighborhood line 16

   Source documentation

   Continuity of factor multiplication supplies the positive compact cell used to turn separated tuples into Haar volume.

   theorem exists_small_factor_tuple_neighborhood
       {N D G : Type*} [Group N] [Group D] [Group G]
       [TopologicalSpace N] [TopologicalSpace D]
       [LocallyCompactSpace N] [LocallyCompactSpace D]
       [MeasurableSpace N] [MeasurableSpace D] [BorelSpace N] [BorelSpace D]
       [MetricSpace G] [IsTopologicalGroup G]
       (ι : N →* G) (κ : D →* G) (hι : Continuous ι) (hκ : Continuous κ)
       (μ : Measure N) (ν : Measure D) [SigmaFinite μ] [SigmaFinite ν]
       [μ.IsOpenPosMeasure] [ν.IsOpenPosMeasure]
       (h : ℕ) {ρ : ℝ} (hρ : 0 < ρ) :
       ∃ U : Set ((Fin h → N) × (Fin h → D)), IsCompact U ∧
         ((Measure.pi fun _ : Fin h => μ).prod (Measure.pi fun _ : Fin h => ν)) U ≠ 0 ∧
   …