WordExponentBounds.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positive common widths for a finite bracket-word list

theorem OAI.PolycyclicRecognition.bracketWordExponent_pos line 15
Source documentation
Every nonempty bracket word has strictly positive width if the letters do.
Distinct definitions of this name: OAI/GroupTheory/PolycyclicRecognition/Geometry/WeightSamplingSupport.lean:33 (different declaration text). Qualify references as OAI.PolycyclicRecognition.bracketWordExponent_pos@path.
```
theorem bracketWordExponent_pos (s : I → ℝ) (hs : ∀ i, 0 < s i)
    (w : FreeMagma I) : 0 < bracketWordExponent s w := by
…
```
Mentions: OAI.PolycyclicRecognition.bracketWordExponent
theorem OAI.PolycyclicRecognition.exists_positive_wordExponent_bounds line 26
Source documentation
The actual finite word list has positive lower width and finite upper width. This supplies the constants in the interior-slack margin.
```
theorem exists_positive_wordExponent_bounds (s : I → ℝ) (hs : ∀ i, 0 < s i)
    (S : Finset (FreeMagma I)) :
    ∃ lo hi : ℝ, 0 < lo ∧ 0 ≤ hi ∧
      ∀ w : S, lo ≤ bracketWordExponent s w ∧ bracketWordExponent s w ≤ hi := by
…
```
Mentions: OAI.PolycyclicRecognition.bracketWordExponent
theorem OAI.PolycyclicRecognition.exists_interior_margin line 43
Source documentation
The free interior constant can always be chosen large enough for the operator-norm proof, while retaining the manuscript's requirement 1 < c.
```
theorem exists_interior_margin (m : ℕ) {lo hi : ℝ} (hlo : 0 < lo) (hhi : 0 ≤ hi) :
    ∃ c : ℝ, 1 < c ∧ (m : ℝ) * hi < c * lo := by
…
```