OAI/GroupTheory/PolycyclicRecognition/Analysis/MeasuredRegionOffset.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.MeasuredProbeRegions.offset_nonpos_of_two_paths line 30

   Source documentation

   Apply the offset count directly to the measured regions produced by Cartan path lifting. All quotient, ideal and Cartan volume bounds are read from those regions; only the source counts and actual paths are supplied.

   theorem MeasuredProbeRegions.offset_nonpos_of_two_paths
       (π : N →* Q) (hπ : Continuous π)
       (μQ : Measure Q) (μI : Measure π.ker) (μ : Measure N) (ν : Measure D)
       [SFinite μQ] [SFinite μI] [SFinite μ] [SFinite ν]
       [μQ.IsMulLeftInvariant] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
       (φ : D →* MulAut N) (ι : N →* G) (κ : D →* G)
       (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
       (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
       (actionQ : D →* MulAut Q) (act : G →* Equiv.Perm Q)
       (hact : ∀ u d q, act (ι u * κ d) q = π u * actionQ d q)
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop) (hscale0 : ∀ n, 0 < scale n)
       (P₂ : ℝ) (R : MeasuredProbeRegions π μQ μI ν scale P₂)
   …

   Mentions: OAI.PolycyclicRecognition.MeasuredProbeRegions