NormalizedWordBrackets.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform normalized structure constants

In a maximizing word basis, the bracket of two basis words is either zero or another word of the finite list. Basis exchange then bounds every scaled bracket coefficient independently of the letter amplitudes.

theorem OAI.PolycyclicRecognition.exists_uniform_normalized_bracket_bound line 25

Source documentation

The algebraic structure-constant bound in the box-calculus lemma.

theorem exists_uniform_normalized_bracket_bound (X : I → L) {k : ℕ}
    (hk : lowerCentralSeries ℝ L L k = ⊥)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (s : I → ℝ)
      (β : WordBasisSelections X (boundedBracketWords k)),
      IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords k) b₀)
        (fun w => bracketWordExponent s w) β.val →
      ∀ (i j l : Fin (finrank ℝ L)) (r : ℝ), 0 ≤ r →
        |(WordBasisSelections.basis X (boundedBracketWords k) β).repr
            ⁅WordBasisSelections.basis X (boundedBracketWords k) β i,
              WordBasisSelections.basis X (boundedBracketWords k) β j⁆ l *
          Real.exp (r * (bracketWordExponent s (β.val i) +
…

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

def OAI.PolycyclicRecognition.exponentialRescaleBasis line 73
Source documentation
The actual rescaled basis whose structure constants are being bounded.
```
def exponentialRescaleBasis {J : Type*} (b : Basis J ℝ L) (cost : J → ℝ) (r : ℝ) :
    Basis J ℝ L :=
…
```
theorem OAI.PolycyclicRecognition.repr_exponentialRescaleBasis_bracket line 78
theorem OAI.PolycyclicRecognition.exists_uniform_rescaled_structureConstant_bound line 100
Source documentation
Uniform boundedness holds for the structure constants of the actual rescaled Lie bracket, not just for a formal coefficient expression.
```
theorem exists_uniform_rescaled_structureConstant_bound (X : I → L) {k : ℕ}
    (hk : lowerCentralSeries ℝ L L k = ⊥)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (s : I → ℝ)
      (β : WordBasisSelections X (boundedBracketWords k)),
      IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords k) b₀)
        (fun w => bracketWordExponent s w) β.val →
      ∀ (r : ℝ), 0 ≤ r →
      let b := exponentialRescaleBasis
…
```
Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.exponentialRescaleBasis