OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceFixedSliceVolume.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.fixedSlice_sequence_volume_exponent_le line 18

   Source documentation

   The geometric packing comparison for compact accessible endpoint sets. Haar volume supplies the lower count; only the image paths and the existing ambient path-packing theorem are used for the upper count.

   theorem fixedSlice_sequence_volume_exponent_le
       {N D G W : Type*} [Group N] [Group D] [Group G]
       [TopologicalSpace N] [MeasurableSpace N] [MeasurableMul N]
       [MetricSpace G] [IsTopologicalGroup G] [IsIsometricSMul G G] [ProperSpace G]
       [NormedAddCommGroup W] [NormedSpace ℝ W] {Λ : ℝ≥0}
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (ι : N →* G) (κ : D →* G) (φ : D →* MulAut N)
       (μ : Measure N) [μ.IsMulLeftInvariant] [IsFiniteMeasureOnCompacts μ]
       (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
       (hconj : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
       (hι : Topology.IsClosedEmbedding ι)
       (S : ℕ → Set N) (hS : ∀ n, IsCompact (S n))
   …