QuotientChainDecay.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Contracting quotient increments along the actual factor lifts

theorem OAI.PolycyclicRecognition.factor_quotient_increment line 16

Source documentation

The quotient increment is the actual Cartan action on the relative ambient increment. Dependence on the nilpotent factor cancels exactly.

theorem factor_quotient_increment
    {N D G Q : Type*} [Group N] [Group D] [Group G] [Group Q]
    (ι : N →* G) (κ : D →* G) (π : N →* Q)
    (α : D →* MulAut Q) (act : G →* Equiv.Perm Q)
    (hact : ∀ n d q, act (ι n * κ d) q = π n * α d q)
    (x y : G) (u : N) (d : D) (hx : ι u * κ d = x) :
    (act x 1)⁻¹ * act y 1 = α d (act (x⁻¹ * y) 1) := by
…

theorem OAI.PolycyclicRecognition.prod_chain_differences line 29

Source documentation

Ordered products of successive differences telescope without commutativity.

theorem prod_chain_differences {Q : Type*} [Group Q] (f : ℕ → Q) (n : ℕ) :
    (List.ofFn (fun i : Fin n => (f i)⁻¹ * f (i + 1))).prod = (f 0)⁻¹ * f n := by
…

theorem OAI.PolycyclicRecognition.quotient_chain_difference_tendsto_one line 46

Source documentation

Polynomially many quotient increments at negative linear height have asymptotically equal endpoints. All increments are the chart logarithms of the actual successive quotients.

theorem quotient_chain_difference_tendsto_one
    (dynkin : NilpotentDynkinExpansionInput E Q)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) Q → Q) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) Q ≃ₜ Q) (hchart : ∀ v, chart v = Exp v)
    {c : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) Q)
      (GroupLieAlgebra (𝓘(ℝ, E)) Q) c = ⊥)
    (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) Q))
    {C : ℝ} (hC : 0 ≤ C) (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C)
    (m : ℕ → ℕ) (f : ℕ → ℕ → Q)
    {A K rate : ℝ} (hA : 0 ≤ A) (hrate : 0 < rate) (p q : ℕ)
    (hcount : ∀ᶠ n in atTop, (m n : ℝ) ≤ K * (1 + (n : ℝ)) ^ q)
    (hstep : ∀ᶠ n in atTop, ∀ i < m n,
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput