OAI/GroupTheory/PolycyclicRecognition/Analysis/ConeProfileOffsetPacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.cone_offset_nonpos_of_profile_cells line 29

   Source documentation

   The sign follows from the two measured affine profiles, the actual anchor-frame Haar law, and the simultaneous coordinate restrictions on thickened cells. No offset multiplier estimate is an assumption.

   theorem cone_offset_nonpos_of_profile_cells
       (π : 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) μ μ)
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop) (hscale0 : ∀ n, 0 < scale n)
   …

   Mentions: OAI.PolycyclicRecognition.quotientSectionHomeomorph