WordChartSmallProducts.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Small products in the actual word-length chart

The bound keeps the sum of the rescaled increment sizes. Thus a word with length small compared with the chart scale has small chart coordinates.

theorem OAI.PolycyclicRecognition.norm_word_chart_coordinates_le line 20

theorem OAI.PolycyclicRecognition.norm_word_chart_change_le line 38

Source documentation

Changing the physical scale by at most a factor of two expands coordinates by at most the largest word degree.

theorem norm_word_chart_change_le
    {L J : Type*} [LieRing L] [LieAlgebra ℝ L] [Fintype J]
    (b : Basis J ℝ L) (cost : J → ℝ) (p : ℕ)
    (hcost : ∀ j, 0 ≤ cost j) (hp : ∀ j, cost j ≤ p)
    {r s : ℝ} (hr : 0 < r) (hs : 0 < s) (hrs : r ≤ 2 * s) (x : L) :
    ‖(exponentialRescaleBasis b cost (Real.log s)).equivFun x‖ ≤
      2 ^ p * ‖(exponentialRescaleBasis b cost (Real.log r)).equivFun x‖ := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis

theorem OAI.PolycyclicRecognition.exists_word_chart_small_product_bound line 69

Source documentation

The constant is independent of the scale and number of increments. Only the published finite Dynkin identity is used.

theorem exists_word_chart_small_product_bound
    (dynkin : NilpotentDynkinExpansionInput E G)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (X : I → L) {c : ℕ} (hc : lowerCentralSeries ℝ L L c = ⊥)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
    (β : WordBasisSelections X (boundedBracketWords c))
    (hβ : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords c) b₀)
      (fun w => bracketWordExponent (fun _ : I => 1) w) β.val) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (r : ℝ), 1 ≤ r → ∀ (n : ℕ) (v : Fin n → L)
      (R : ℝ), 0 ≤ R →
      (∀ i, ‖(WordBasisSelections.basis X (boundedBracketWords c) β).equivFun (v i)‖ ≤ R) →
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.WordBasisSelections.basis