SequenceSmallExponentialProducts.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The logarithm of a bounded probe section times a small generator

theorem OAI.PolycyclicRecognition.exists_sequence_small_product_bound line 22

Source documentation

A two-factor Dynkin product multiplies the small exponential rate only by its fixed degree. The remaining radius is subexponential.

theorem exists_sequence_small_product_bound
    (e : V ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) N)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) N → N) (hExp : IsGroupExponential Exp)
    (dynkin : NilpotentDynkinExpansionInput E N)
    {c : ℕ} (hc : lowerCentralSeries ℝ V V c = ⊥) (b : Basis J ℝ V)
    (scale R₁ R₂ : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (hscale0 : ∀ n, 0 ≤ scale n) (hR₁0 : ∀ n, 0 ≤ R₁ n) (hR₂0 : ∀ n, 0 ≤ R₂ n)
    (hR₁ : HasSubexponentialUpperBoundSeq scale R₁)
    (hR₂ : HasSubexponentialUpperBoundSeq scale R₂) :
    ∃ R : ℕ → ℝ, (∀ n, 0 ≤ R n) ∧ HasSubexponentialUpperBoundSeq scale R ∧
      ∀ n (δ : ℝ), 0 ≤ δ → ∀ x y : V,
        ‖b.equivFun x‖ ≤ R₁ n → ‖b.equivFun y‖ ≤ R₂ n * Real.exp (δ * scale n) →
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq