OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceConeQuotientBoxes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_sequence_cone_quotient_envelope line 22

   Source documentation

   The actual cone quotient sends all first-sheet boxes, at every scale and in every selected word basis, into one common sequence of quotient log boxes of subexponential Haar volume. The measure can be the one already chosen for the quotient Jacobian.

   theorem exists_sequence_cone_quotient_envelope
       {N : Type*} [Group N] (ExpN : cartanRootIdeal H → N)
       (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
       (ExpQ : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier → Q.carrier)
       (hExpQ : IsGroupExponential ExpQ)
       (haar : NilpotentExponentialHaarInput Q.modelSpace Q.carrier)
       (π : N →* Q.carrier)
       (hπ : ∀ v, π (ExpN v) = ExpQ (Q.equiv (M.coneProjection C v)))
       {k : ℕ} (bQ : Basis (Fin k) ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
       (μ : Measure Q.carrier) [μ.IsHaarMeasure]
       (scale R : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
       (hR0 : ∀ n, 0 ≤ R n) (hR : HasSubexponentialUpperBoundSeq scale R) :
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq