BoxWordExpansion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite word coefficients of an actual enlarged box point

theorem OAI.PolycyclicRecognition.exists_word_expansion_of_rescaled_norm_le line 17

Source documentation

Membership in a scaled word box supplies a finite expansion with a common coefficient bound. Repetitions are harmless; the dimension factor also covers them without any uniqueness requirement.

theorem exists_word_expansion_of_rescaled_norm_le
    {I L : Type*} [LieRing L] [LieAlgebra ℝ L]
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (cost : S → ℝ) (r : ℝ) {R : ℝ} (hR : 0 ≤ R) (v : L)
    (hv : ‖(exponentialRescaleBasis (WordBasisSelections.basis X S β)
      (fun i => cost (β.val i)) r).equivFun v‖ ≤ R) :
    ∃ a : S → ℝ,
      (∀ w, |a w| ≤ (finrank ℝ L : ℝ) * R * Real.exp (r * cost w)) ∧
      ∑ w, a w • evalBracketWord X w = v := by
…

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

theorem OAI.PolycyclicRecognition.exists_word_expansion_of_enlarged_box line 70

Source documentation

The deterministic enlarged suffix has precisely the coefficient envelope used by interior slack. Its subexponential radius is retained.

theorem exists_word_expansion_of_enlarged_box
    {I L : Type*} [LieRing L] [LieAlgebra ℝ L]
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (cost : S → ℝ) (r δ ε : ℝ) (v : L)
    (hv : ‖(exponentialRescaleBasis (WordBasisSelections.basis X S β)
      (fun i => (1 + δ) * cost (β.val i)) r).equivFun v‖ ≤ Real.exp (r * ε)) :
    ∃ a : S → ℝ,
      (∀ w, |a w| ≤ (finrank ℝ L : ℝ) *
        Real.exp (r * ((1 + δ) * cost w + ε))) ∧
      ∑ w, a w • evalBracketWord X w = v := by
…