WordChartLeftShift.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exact changes of basepoint in nilpotent exponential coordinates

def OAI.PolycyclicRecognition.exponentialCoordinates line 21

Source documentation

Coordinates use the given global exponential chart and the actual chosen basis; no topology on the abstract Lie algebra is needed.

def exponentialCoordinates {n : ℕ}
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G)
    (b : Basis (Fin n) ℝ L) : (Fin n → ℝ) ≃ₜ G :=
…

theorem OAI.PolycyclicRecognition.exponentialCoordinates_apply line 28

def OAI.PolycyclicRecognition.wordChartLeftShift line 35

Source documentation

The chart change determined by left multiplication by k⁻¹.

def wordChartLeftShift {n : ℕ}
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G)
    (source target : Basis (Fin n) ℝ L) (k : G) :
    C((Fin n → ℝ), (Fin n → ℝ)) where
…

theorem OAI.PolycyclicRecognition.wordChartLeftShift_point line 45
theorem OAI.PolycyclicRecognition.wordChartLeftShift_change_basis line 53

theorem OAI.PolycyclicRecognition.exists_wordChartLeftShift_norm_bound line 69

Source documentation

The exact group-defined shift satisfies the polynomial chart bound.

theorem exists_wordChartLeftShift_norm_bound
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ v, chart v = Exp v)
    (X : I → L) {d : ℕ} (hd : lowerCentralSeries ℝ L L d = ⊥)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
    (β : WordBasisSelections X (boundedBracketWords d))
    (hβ : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords d) b₀)
      (fun w => bracketWordExponent (fun _ : I => 1) w) β.val)
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (e (finiteDynkinPolynomial a ![x, y])) = Exp (e x) * Exp (e y))
    (R : ℝ) :
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial

theorem OAI.PolycyclicRecognition.exists_wordChartLeftShift_ball line 106

Source documentation

A fixed smaller ball is carried into the prescribed chart ball when the normalized Cartan shift is small and the scales differ by at most two.

theorem exists_wordChartLeftShift_ball
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ v, chart v = Exp v)
    (X : I → L) {d : ℕ} (hd : lowerCentralSeries ℝ L L d = ⊥)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
    (β : WordBasisSelections X (boundedBracketWords d))
    (hβ : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords d) b₀)
      (fun w => bracketWordExponent (fun _ : I => 1) w) β.val)
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (e (finiteDynkinPolynomial a ![x, y])) = Exp (e x) * Exp (e y))
    {R : ℝ} (hR : 0 < R) :
…

theorem OAI.PolycyclicRecognition.wordChartLeftShift_height line 174

Source documentation

Height under this change of basepoint is exactly affine, at the two physical scales. This identity is separate from metric compatibility.

theorem wordChartLeftShift_height
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G)
    (π : G →* Multiplicative W) (height : L →ₗ[ℝ] W)
    (hheight : ∀ v, (π (chart (e v))).toAdd = height v)
    (hkill : ∀ x y : L, height ⁅x, y⁆ = 0)
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    {r s : ℝ} (hr : 0 < r) (hs : 0 < s) (k : G)
    (z : Fin (finrank ℝ L) → ℝ) :
    let b := WordBasisSelections.basis X S β
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.WordBasisSelections.basis