DynkinSummableProducts.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite BCH products controlled by the sum of input sizes

The coefficient bound in the existing finite Dynkin input also controls products by the sum of the logarithmic input norms. In particular the bound tends to zero with that sum, independently of the number of factors. This is the estimate needed for contracting quotient trajectories in exponential coordinates; no Riemannian metric comparison is assumed.

theorem OAI.PolycyclicRecognition.norm_rightNestedWord_le_product line 25

Source documentation

Keep the individual letter sizes when estimating a right-nested word.

theorem norm_rightNestedWord_le_product (b : Basis J ℝ L)
    {I : Type*} (X : I → L) {C : ℝ} (hC : 0 ≤ C)
    (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C)
    (d : ℕ) (w : Fin (d + 1) → I) :
    ‖b.equivFun (evalBracketWord X (rightNestedWord d w))‖ ≤
      ((Fintype.card J : ℝ) ^ 2 * C) ^ d * ∏ i, ‖b.equivFun (X (w i))‖ := by
…

Mentions: OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.rightNestedWord

theorem OAI.PolycyclicRecognition.norm_finiteDynkinPolynomial_le_sum line 51

Source documentation

The finite Dynkin polynomial is bounded by a polynomial in the sum of input norms, with zero constant term.

theorem norm_finiteDynkinPolynomial_le_sum (b : Basis J ℝ L) {c n : ℕ}
    (coeff : DynkinCoefficients c n) (hcoeff : ∀ d w, |coeff d w| ≤ (2 : ℝ) ^ c)
    (X : Fin n → L) {C : ℝ} (hC : 0 ≤ C)
    (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C) :
    ‖b.equivFun (finiteDynkinPolynomial coeff X)‖ ≤
      (c : ℝ) * 2 ^ c * (1 + (Fintype.card J : ℝ) ^ 2 * C) ^ c *
        (∑ i, ‖b.equivFun (X i)‖) * (1 + ∑ i, ‖b.equivFun (X i)‖) ^ c := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial

theorem OAI.PolycyclicRecognition.exists_product_log_with_sum_bound line 111

Source documentation

Actual finite products of exponentials have a logarithm controlled by the total input size, independently of the number of factors.

theorem exists_product_log_with_sum_bound
    (dynkin : NilpotentDynkinExpansionInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    {c n : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)
      (GroupLieAlgebra (𝓘(ℝ, E)) G) c = ⊥)
    (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G))
    {C : ℝ} (hC : 0 ≤ C)
    (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C)
    (X : Fin n → GroupLieAlgebra (𝓘(ℝ, E)) G) :
    ∃ z, (List.ofFn (fun i => Exp (X i))).prod = Exp z ∧
      ‖b.equivFun z‖ ≤
        (c : ℝ) * 2 ^ c * (1 + (Fintype.card J : ℝ) ^ 2 * C) ^ c *
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput