OAI/GroupTheory/PolycyclicRecognition/Analysis/FixedSliceVolumeComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.fixedSlice_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_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}
       (ι : 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 : ∀ r, IsCompact (S r))
       (x : ℝ → G) (d : ℝ → D) (a : ℝ → G) (f : ℝ → NormalizedPair G Λ)
   …

   Mentions: OAI.PolycyclicRecognition.NormalizedPair