WordBallLeftShift.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compact-ball restriction of the actual changed-center chart

def OAI.PolycyclicRecognition.wordBallLeftShift line 20

Source documentation

The genuine group-defined shift, with its range restricted by the proved chart bound.

def wordBallLeftShift {n : ℕ}
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G)
    (source target : Basis (Fin n) ℝ L) (k : G) (R S : ℝ)
    (hbound : ∀ z : Fin n → ℝ, ‖z‖ ≤ R →
      ‖wordChartLeftShift e chart source target k z‖ ≤ S) :
    C(closedBall (0 : Fin n → ℝ) R, closedBall (0 : Fin n → ℝ) S) := by
…

Mentions: OAI.PolycyclicRecognition.wordChartLeftShift

theorem OAI.PolycyclicRecognition.wordChartLeftShift_normalized_height line 38

Source documentation

Normalizing the exact two-scale height identity produces the affine translation required by the finite-label comparison.

theorem wordChartLeftShift_normalized_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