SequenceDifferenceWordImage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One fixed switch scheme retains volume on every sufficiently large good set

theorem OAI.PolycyclicRecognition.differenceWord_subexponential_image_sequence line 15

theorem OAI.PolycyclicRecognition.exists_fixed_differenceWord_image_sequence line 45

Source documentation

The scheme is fixed before the successful parameter sets are selected. Its limiting rank follows from the generating Lie words, not from any premise on the restricted endpoint images.

theorem exists_fixed_differenceWord_image_sequence
    {I J : Type*} [Fintype I] {n c : ℕ}
    (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
    (rem : RemezPolynomialInput) (hn : 1 ≤ n) (a : DynkinCoefficients c 2)
    (S : Set (((Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) × (I → Fin n → ℝ)))
    (hS : IsCompact S)
    (b : ℕ → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) × (I → Fin n → ℝ))
    (hb : ∀ r, b r ∈ S)
    (b₀ : ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) × (I → Fin n → ℝ))
    (hb₀ : b₀ ∈ S) (hlim : Tendsto b atTop (𝓝 b₀))
    (hB : IsLieBracket b₀.1) (hg : PolynomialGroupLaws (dynkinProduct a b₀.1))
    (hc : ExponentialConjugationLaw (dynkinProduct a b₀.1) b₀.1)
…

Mentions: OAI.PolycyclicRecognition.RemezPolynomialInput, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.ExponentialConjugationLaw