CartanProductCoordinates.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Coordinates of Cartan support positions

The actual product of a pivot and a scaled support direction has polynomial logarithmic coordinates. This uses only the finite published Dynkin identity; it does not identify multiplication with vector addition.

theorem OAI.PolycyclicRecognition.exists_cartan_mul_log_bound line 28

Source documentation

Polynomial coordinates of the actual product of two Cartan exponentials.

theorem exists_cartan_mul_log_bound
    (hExpD : IsGroupExponential ExpD) (dynkinD : NilpotentDynkinExpansionInput ED D) :
    ∃ (C : ℝ) (c : ℕ), 0 ≤ C ∧ ∀ x y : H,
      ‖(finBasis ℝ H).equivFun
        (cartanLog H eD ExpD hbijD (ExpD (eD x) * ExpD (eD y)))‖ ≤
      C * (1 + ‖(finBasis ℝ H).equivFun x‖ + ‖(finBasis ℝ H).equivFun y‖) ^ c := by
…

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

theorem OAI.PolycyclicRecognition.exists_cartan_scaled_mul_log_bound line 60

Source documentation

A polynomially bounded pivot remains polynomially bounded after every scaled support visit. The exponent and constant are uniform over the pivot.

theorem exists_cartan_scaled_mul_log_bound
    (hExpD : IsGroupExponential ExpD) (dynkinD : NilpotentDynkinExpansionInput ED D)
    {A V : ℝ} (hA : 0 ≤ A) (hV : 0 ≤ V) (p : ℕ) :
    ∃ (C : ℝ) (q : ℕ), 0 ≤ C ∧ ∀ (r : ℝ), 0 ≤ r → ∀ h v : H,
      ‖(finBasis ℝ H).equivFun h‖ ≤ A * (1 + r) ^ p →
      ‖(finBasis ℝ H).equivFun v‖ ≤ V →
      ‖(finBasis ℝ H).equivFun
        (cartanLog H eD ExpD hbijD (ExpD (eD h) * ExpD (eD (r • v))))‖ ≤
        C * (1 + r) ^ q := by
…

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