OAI/GroupTheory/PolycyclicRecognition/Analysis/SmallFactorCell.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_small_factor_cell line 17

   Source documentation

   This cell is chosen before the Haar normalization used by a probe region. Its interior contains the identity, so every product Haar measure gives it positive finite mass.

   theorem exists_small_factor_cell
       {N D G : Type*} [Group N] [Group D] [Group G]
       [TopologicalSpace N] [TopologicalSpace D]
       [LocallyCompactSpace N] [LocallyCompactSpace D]
       [MetricSpace G] [IsTopologicalGroup G]
       (ι : N →* G) (κ : D →* G) (hι : Continuous ι) (hκ : Continuous κ) :
       ∃ U : Set (N × D), IsCompact U ∧ (1 : N × D) ∈ interior U ∧
         ∀ z ∈ U, dist (1 : G) (ι z.1 * κ z.2) < 1 / 2 := by
   …

2. theorem OAI.PolycyclicRecognition.small_factor_cell_measure line 34

   Source documentation

   The same fixed cell works for each of the section-dependent Haar products appearing in the target comparison.

   theorem small_factor_cell_measure
       {N D : Type*} [TopologicalSpace N] [TopologicalSpace D]
       [T2Space N] [T2Space D]
       [SecondCountableTopology N] [SecondCountableTopology D]
       [MeasurableSpace N] [MeasurableSpace D] [BorelSpace N] [BorelSpace D]
       (μ : Measure N) (ν : Measure D) [SFinite μ] [SFinite ν]
       [μ.IsOpenPosMeasure] [ν.IsOpenPosMeasure]
       [IsFiniteMeasureOnCompacts μ] [IsFiniteMeasureOnCompacts ν]
       {U : Set (N × D)} (hU : IsCompact U) (hne : (interior U).Nonempty) :
       MeasurableSet U ∧ (μ.prod ν) U ≠ 0 ∧ (μ.prod ν) U ≠ ⊤ := by
   …