SequenceCartanProducts.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Products of the Cartan factors of two probe paths

theorem OAI.PolycyclicRecognition.exists_sequence_cartan_product_bound line 24

Source documentation

A common subexponential box contains the products of every allowed pair of Cartan factors, including the final right-cell increment.

theorem exists_sequence_cartan_product_bound
    (hExpD : IsGroupExponential ExpD) (dynkinD : NilpotentDynkinExpansionInput ED D)
    (scale R₁ R₂ : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (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 (d e : D),
        ‖(finBasis ℝ H).equivFun (cartanLog H eD ExpD hbijD d)‖ ≤ R₁ n →
        ‖(finBasis ℝ H).equivFun (cartanLog H eD ExpD hbijD e)‖ ≤ R₂ n →
        ‖(finBasis ℝ H).equivFun (cartanLog H eD ExpD hbijD (d * e))‖ ≤ R n := by
…

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