BoundedGeneratorSchemes.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative bounds for a fixed generator scheme

The fixed conjugating words give a common amplitude bound; scaling a logarithm into the local product chart and repeating the resulting word covers any prescribed bounded logarithmic set.

theorem OAI.PolycyclicRecognition.exists_fixed_word_amplitude_bound line 22
Source documentation
Amplitudes in every fixed conjugating word admit one finite bound.
```
theorem exists_fixed_word_amplitude_bound {n : ℕ} (w : Fin n → List (I × ℝ)) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ k, ∀ p ∈ w k, |p.2| ≤ C := by
…
```

theorem OAI.PolycyclicRecognition.generatorSchemeWord_amplitude_bound line 39

Source documentation

Inserting unit-bounded parameters keeps every amplitude uniformly bounded.

theorem generatorSchemeWord_amplitude_bound {n : ℕ} (w : Fin n → List (I × ℝ))
    (i : Fin n → I) {C : ℝ} (hC : 1 ≤ C)
    (hw : ∀ k, ∀ p ∈ w k, |p.2| ≤ C) (t : Fin n → ℝ) (ht : ‖t‖ ≤ 1) :
    ∀ p ∈ generatorSchemeWord w i t, |p.2| ≤ C := by
…

Mentions: OAI.PolycyclicRecognition.generatorSchemeWord

theorem OAI.PolycyclicRecognition.exp_nat_smul line 68

Source documentation

The one-parameter identity identifies integer multiples with group powers.

theorem exp_nat_smul (hzero : Exp 0 = 1)
    (hadd : ∀ v (s t : ℝ), Exp ((s + t) • v) = Exp (s • v) * Exp (t • v))
    (v : L) (k : ℕ) : Exp ((k : ℝ) • v) = (Exp v) ^ k := by
…

theorem OAI.PolycyclicRecognition.bounded_generation_of_local_scheme line 77

Source documentation

Any bounded logarithmic set is covered by words of uniformly bounded length and uniformly bounded generator amplitudes, for a fixed local scheme.

theorem bounded_generation_of_local_scheme {n : ℕ}
    (w : Fin n → List (I × ℝ)) (i : Fin n → I)
    (hzero : Exp 0 = 1)
    (hadd : ∀ v (s t : ℝ), Exp ((s + t) • v) = Exp (s • v) * Exp (t • v))
    {ε : ℝ} (hε : 0 < ε)
    (hlocal : ∀ v : L, ‖v‖ < ε → ∃ t : Fin n → ℝ, ‖t‖ < 1 ∧
      generatorGroupWord X Exp (generatorSchemeWord w i t) = Exp v)
    (R : ℝ) :
    ∃ (N : ℕ) (C : ℝ), 1 ≤ C ∧ ∀ v : L, ‖v‖ ≤ R →
      ∃ u : List (I × ℝ), u.length ≤ N ∧ (∀ p ∈ u, |p.2| ≤ C) ∧
        generatorGroupWord X Exp u = Exp v := by
…

Mentions: OAI.PolycyclicRecognition.generatorGroupWord, OAI.PolycyclicRecognition.generatorSchemeWord