OAI/GroupTheory/PolycyclicRecognition/Analysis/FactorProductVolumeBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.factor_separated_card_le_product_volume line 19

   Source documentation

   Fixed positive lifted cells convert a product-volume estimate into a separated endpoint count. The factor projection need not be injective.

   theorem factor_separated_card_le_product_volume (φ : D →* MulAut N)
       (ι : N →* G) (κ : D →* G)
       (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
       (μ : Measure N) (ν : Measure D) [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
       [SFinite μ] [SFinite ν] (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
       (s : Finset G) (p : G → N × D) (U : Set (N × D)) (E : Set N) (B : Set D)
       (hU : MeasurableSet U) (hU0 : (μ.prod ν) U ≠ 0) (hUtop : (μ.prod ν) U ≠ ⊤)
       (hE : μ E ≠ ⊤) (hB : ν B ≠ ⊤) {ρ : ℝ}
       (hp : ∀ x ∈ s, ι (p x).1 * κ (p x).2 = x)
       (hsmall : ∀ z ∈ U, dist (1 : G) (ι z.1 * κ z.2) < ρ / 2)
       (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ρ ≤ dist x y)
       (hthick : ∀ x ∈ s, factorTranslate φ (p x) '' U ⊆ E ×ˢ B) :
   …

   Mentions: OAI.PolycyclicRecognition.factorTranslate