OAI/GroupTheory/PolycyclicRecognition/Analysis/ConditionedGoodProbeOffset.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.MeasuredProbeRegions.offset_nonpos_of_conditioned_probes line 36

   Source documentation

   The compact good set from the original section-product probability supplies both the source lower count and the finite tile cover. The only remaining geometric premises are the actual paths, short bridge, and Haar restrictions.

   theorem MeasuredProbeRegions.offset_nonpos_of_conditioned_probes
       (π : N →* Q) (hπ : Continuous π)
       (μQ : Measure Q) (μI : Measure π.ker) (μ : Measure N) (ν : Measure D)
       [SFinite μQ] [SFinite μI] [SFinite μ] [SFinite ν]
       [μQ.IsMulLeftInvariant] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
       [μI.IsMulRightInvariant]
       [IsFiniteMeasureOnCompacts μ]
       (φ : 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)
   …