RescaledGeneratorBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for normalized generator vectors

The same maximizing-basis exchange estimate which bounds structure constants also bounds all exponentially rescaled generator vectors. Thus both parts of the normalized Lie-law data lie in fixed bounded coordinate sets.

theorem OAI.PolycyclicRecognition.repr_exponentialRescaleBasis_smul line 22

Source documentation

Coordinates of a scalar-rescaled vector in an exponentially rescaled basis.

theorem repr_exponentialRescaleBasis_smul {J : Type*} (b : Basis J ℝ L)
    (cost : J → ℝ) (r s : ℝ) (x : L) (j : J) :
    (exponentialRescaleBasis b cost r).repr (Real.exp (r * s) • x) j =
      b.repr x j * Real.exp (r * (s - cost j)) := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis

theorem OAI.PolycyclicRecognition.exists_uniform_rescaled_generator_bound line 39

Source documentation

Uniform boundedness of all rescaled letters in every maximizing word basis.

theorem exists_uniform_rescaled_generator_bound
    (X : I → L) (S : Finset (FreeMagma I))
    (hS : ∀ i, FreeMagma.of i ∈ S) (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (s : I → ℝ) (β : WordBasisSelections X S),
      IsMaximizingColumnBasis (wordListCoordinates X S b₀)
        (fun w => bracketWordExponent s w) β.val →
      ∀ r : ℝ, 0 ≤ r → ∀ i,
      ‖(exponentialRescaleBasis (WordBasisSelections.basis X S β)
        (fun j => bracketWordExponent s (β.val j)) r).equivFun
          (Real.exp (r * s i) • X i)‖ ≤ C := by
…

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