RescaledWordSums.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exponential bounds for actual finite word expansions

The maximizing-basis exchange estimate controls every word in the finite list. A common surplus or deficit in the coefficients passes to the norm of the whole sum, uniformly over the selected maximizing basis.

theorem OAI.PolycyclicRecognition.exists_uniform_rescaled_word_bound line 23

Source documentation

All words, rather than just the original letters, have uniformly bounded coordinates after normalization by their own weight.

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

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

theorem OAI.PolycyclicRecognition.norm_rescaled_word_sum_le line 48

Source documentation

A finite expansion with a common exponential margin retains that margin in the actual normalized coordinate norm. The index may repeat words.

theorem norm_rescaled_word_sum_le
    {J : Type*} [Fintype J]
    (X : I → L) (S : Finset (FreeMagma I))
    (b : Basis (Fin (finrank ℝ L)) ℝ L)
    (cost : S → ℝ) (r : ℝ) {C R θ : ℝ} (hR : 0 ≤ R)
    (hword : ∀ w : S, ‖b.equivFun
      (Real.exp (r * cost w) • evalBracketWord X w)‖ ≤ C)
    (w : J → S) (a : J → ℝ)
    (ha : ∀ j, |a j| ≤ R * Real.exp (r * (cost (w j) + θ))) :
    ‖b.equivFun (∑ j, a j • evalBracketWord X (w j))‖ ≤
      (Fintype.card J : ℝ) * C * R * Real.exp (r * θ) := by
…

Mentions: OAI.PolycyclicRecognition.evalBracketWord