DifferenceWordImage.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 line 14

theorem OAI.PolycyclicRecognition.exists_fixed_differenceWord_image line 43

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
    {I J : Type*} [Fintype I] {n c : ℕ}
    (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)
    (basis : Basis J ℝ (Fin n → ℝ)) (words : J → FreeMagma I)
…

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