OAI/GroupTheory/PolycyclicRecognition/Analysis/WordChartLogBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.wordChartLeftShift_zero_log line 20

   Source documentation

   The shift of zero is the negative logarithm of the translating element, expressed in the target basis.

   theorem wordChartLeftShift_zero_log
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
       (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ v, chart v = Exp v)
       {n : ℕ} (source target : Basis (Fin n) ℝ L) (k : G) :
       ∃ h : L, Exp (e h) = k ∧
         ‖target.equivFun h‖ = ‖wordChartLeftShift e chart source target k 0‖ := by
   …

   Mentions: OAI.PolycyclicRecognition.wordChartLeftShift

2. theorem OAI.PolycyclicRecognition.exists_wordChartLeftShift_log_bound line 37

   Source documentation

   A bounded point in the word-length rescaled chart has a polynomially bounded logarithm in any fixed reference basis.

   theorem exists_wordChartLeftShift_log_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)
       [Fintype I] [DecidableEq I] (X : I → L) (d : ℕ)
       (β : WordBasisSelections X (boundedBracketWords d))
       (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) :
       ∃ (C : ℝ) (p : ℕ), 0 ≤ C ∧ ∀ r : ℝ, 1 ≤ r →
         let br := exponentialRescaleBasis (WordBasisSelections.basis X (boundedBracketWords d) β)
   …

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