FiniteDynkinDifference.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Difference bounds for the actual finite Dynkin polynomial

The middle input in a conjugation product vanishes at time zero. These bounds retain that factor rather than losing it in an absolute polynomial estimate; this gives polynomial coarse speed for Cartan-fiber paths.

theorem OAI.PolycyclicRecognition.norm_basis_evalBracketWord_sub_le line 23

Source documentation

A bracket word is Lipschitz on a coordinate ball, with one fewer power of its radius than the absolute word bound.

theorem norm_basis_evalBracketWord_sub_le
    (X Y : I → L) {C M D : ℝ} (hC : 0 ≤ C) (hM : 0 ≤ M) (hD : 0 ≤ D)
    (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C)
    (hX : ∀ i, ‖b.equivFun (X i)‖ ≤ M) (hY : ∀ i, ‖b.equivFun (Y i)‖ ≤ M)
    (hXY : ∀ i, ‖b.equivFun (X i - Y i)‖ ≤ D) (w : FreeMagma I) :
    ‖b.equivFun (evalBracketWord X w - evalBracketWord Y w)‖ ≤
      (bracketWordLength w : ℝ) * ((Fintype.card J : ℝ) ^ 2 * C) ^ bracketWordNodes w *
        M ^ bracketWordNodes w * D := by
…

Mentions: OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.bracketWordLength, OAI.PolycyclicRecognition.bracketWordNodes

theorem OAI.PolycyclicRecognition.exists_finiteDynkinPolynomial_difference_bound line 69

Source documentation

Fixed finite Dynkin coefficients give a uniform polynomial Lipschitz bound on coordinate balls. No extra group-law or analytic input is used.

theorem exists_finiteDynkinPolynomial_difference_bound
    {c n : ℕ} (a : DynkinCoefficients c n) {C : ℝ} (hC : 0 ≤ C)
    (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (X Y : Fin n → L) (M D : ℝ), 0 ≤ M → 0 ≤ D →
      (∀ i, ‖b.equivFun (X i)‖ ≤ M) → (∀ i, ‖b.equivFun (Y i)‖ ≤ M) →
      (∀ i, ‖b.equivFun (X i - Y i)‖ ≤ D) →
      ‖b.equivFun (finiteDynkinPolynomial a X - finiteDynkinPolynomial a Y)‖ ≤
        A * (1 + M) ^ c * D := by
…

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