UniformDynkinDifference.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A common translation bound for every word-chart scale

theorem OAI.PolycyclicRecognition.exists_uniform_finiteDynkinPolynomial_difference_bound line 18

Source documentation

The difference constant depends on the coefficient bound for the bracket, so a bounded family of coordinate brackets shares one constant.

theorem exists_uniform_finiteDynkinPolynomial_difference_bound
    {c n : ℕ} (a : DynkinCoefficients c n) {C : ℝ} (hC : 0 ≤ C) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ b : Basis J ℝ L,
      (∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C) →
      ∀ (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