OAI/GroupTheory/PolycyclicRecognition/Analysis/ConeProbeRestrictionPacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.cone_offset_nonpos_of_probe_restrictions line 28

   Source documentation

   A quotient restriction in the first sheet and an ideal restriction in the second sheet combine for the same thickened endpoints. The containing product regions and translated quotient coordinates are constructed here.

   theorem cone_offset_nonpos_of_probe_restrictions
       (π : N →* Q) (hπ : Continuous π) (σ : C(Q, N))
       (hs : ∀ q, π (σ q) = q)
       (μQ : Measure Q) (μI : Measure π.ker) (μ : Measure N) (ν : Measure D)
       [SFinite μQ] [SFinite μI] [SFinite μ] [SFinite ν]
       [μQ.IsMulLeftInvariant] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
       (hμ : μ = Measure.map (quotientSectionHomeomorph π hπ σ hs).symm
         (μQ.prod μI))
       (φ : 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)
   …

   Mentions: OAI.PolycyclicRecognition.quotientSectionHomeomorph