WordChartPivot.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial size and exact height of a scaled word-chart pivot

def OAI.PolycyclicRecognition.wordChartPivot line 13

theorem OAI.PolycyclicRecognition.wordChartPivot_polynomial_bound line 22

Source documentation

The pivot logarithm has one fixed polynomial envelope in the physical scale, for the actual fixed word chart and coordinate.

theorem wordChartPivot_polynomial_bound {L I : Type*} [LieRing L] [LieAlgebra ℝ L]
    [Fintype I] [DecidableEq I] [FiniteDimensional ℝ L]
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (z : Fin (finrank ℝ L) → ℝ) :
    ∃ A : ℝ, ∃ p : ℕ, 0 ≤ A ∧ ∀ r : ℝ, 1 ≤ r →
      ‖b₀.equivFun (wordChartPivot X S β r z)‖ ≤ A * (1 + r) ^ p := by
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.wordChartPivot

theorem OAI.PolycyclicRecognition.wordChartPivot_height line 41

Source documentation

The pivot's height is exactly linear in physical scale.

theorem wordChartPivot_height {L W I : Type*} [LieRing L] [LieAlgebra ℝ L]
    [AddCommGroup W] [Module ℝ W] [Fintype I] [DecidableEq I]
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (h : L →ₗ[ℝ] W) (hh : ∀ x y : L, h ⁅x, y⁆ = 0)
    {r : ℝ} (hr : 1 ≤ r) (z : Fin (finrank ℝ L) → ℝ) :
    h (wordChartPivot X S β r z) =
      r • h ((WordBasisSelections.basis X S β).equivFun.symm z) := by
…

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