NilpotentBoxes.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Products in actual nilpotent exponential boxes

The published finite BCH identity is transported to a chosen Lie-algebra model. The uniform normalized structure constants then give the polynomial product bound in the manuscript's box calculus, for every height scale and letter support. No coordinate growth conclusion is assumed as an input.

def OAI.PolycyclicRecognition.exponentialCoordinateBox line 25
Source documentation
The exponential image of the coordinate cube of radius R. With the supremum norm on the coordinate functions this is exactly the usual box.
```
def exponentialCoordinateBox {G J : Type*} [Fintype J]
    (exp : L → G) (b : Basis J ℝ L) (R : ℝ) : Set G :=
…
```
theorem OAI.PolycyclicRecognition.mem_exponentialCoordinateBox_iff line 29

theorem OAI.PolycyclicRecognition.model_finiteDynkinExpansion line 49

Source documentation

Transport only the finite expansion needed by the model.

theorem model_finiteDynkinExpansion
    (dynkin : NilpotentDynkinExpansionInput E G)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    {c : ℕ} (hc : lowerCentralSeries ℝ L L c = ⊥) (n : ℕ) :
    ∃ coeff : DynkinCoefficients c n, (∀ d w, |coeff d w| ≤ (2 : ℝ) ^ c) ∧
      ∀ X : Fin n → L, (List.ofFn (fun i => Exp (e (X i)))).prod =
        Exp (e (finiteDynkinPolynomial coeff X)) := by
…

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

theorem OAI.PolycyclicRecognition.product_mem_exponentialCoordinateBox line 67

Source documentation

The polynomial product estimate in any basis with bounded brackets.

theorem product_mem_exponentialCoordinateBox
    (dynkin : NilpotentDynkinExpansionInput E G)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    {c n : ℕ} (hc : lowerCentralSeries ℝ L L c = ⊥)
    {J : Type*} [Fintype J] (b : Basis J ℝ L)
    {C R : ℝ} (hC : 0 ≤ C) (hR : 0 ≤ R)
    (hbracket : ∀ i j l, |b.repr ⁅b i, b j⁆ l| ≤ C)
    (g : Fin n → G) (hg : ∀ i, g i ∈ exponentialCoordinateBox (Exp ∘ e) b R) :
    (List.ofFn g).prod ∈ exponentialCoordinateBox (Exp ∘ e) b
      ((c : ℝ) * 2 ^ c * (1 + (Fintype.card J : ℝ) ^ 2 * C) ^ c *
        (1 + R) ^ c * (1 + (n : ℝ)) ^ c) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.exponentialCoordinateBox

theorem OAI.PolycyclicRecognition.inv_mem_exponentialCoordinateBox line 87

Source documentation

Inversion preserves every exponential coordinate box exactly.

theorem inv_mem_exponentialCoordinateBox
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    {J : Type*} [Fintype J] (b : Basis J ℝ L) {R : ℝ} {g : G}
    (hg : g ∈ exponentialCoordinateBox (Exp ∘ e) b R) :
    g⁻¹ ∈ exponentialCoordinateBox (Exp ∘ e) b R := by
…

Mentions: OAI.PolycyclicRecognition.exponentialCoordinateBox

theorem OAI.PolycyclicRecognition.exists_uniform_word_box_product_bound line 102

Source documentation

Uniform polynomial multiplication in all maximizing scaled word boxes. The constant depends only on the fixed finite Lie model.

theorem exists_uniform_word_box_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) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (s : I → ℝ)
      (β : WordBasisSelections X (boundedBracketWords c)),
      IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords c) b₀)
        (fun w => bracketWordExponent s w) β.val →
      ∀ r : ℝ, 0 ≤ r → ∀ n : ℕ, ∀ R : ℝ, 0 ≤ R → ∀ g : Fin n → G,
      let b := exponentialRescaleBasis (WordBasisSelections.basis X (boundedBracketWords c) β)
…

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