SupportWordImage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Image control from the actual prefix sheets of a generator word

The hypotheses concern only the finitely many sheets visited by the chosen word. They do not ask for a good profile at every possible starting point.

theorem OAI.PolycyclicRecognition.indexedWordProduct_append line 23

theorem OAI.PolycyclicRecognition.supportWordPath_bound_of_prefixes line 29

Source documentation

Finitely many estimates at the actual prefixes suffice for the whole explicit word path, with the usual uniform concatenation constant.

theorem supportWordPath_bound_of_prefixes
    {S : Set G} {L κ : ℝ} (hL : 0 ≤ L) (hκ : 0 ≤ κ)
    (u : List (I × ℝ)) (n : G) (hbase : n * d₀ ∈ S)
    (hvisit : ∀ (v : List (I × ℝ)) (i : I) (b : ℝ) (w : List (I × ℝ)),
      u = v ++ (i, b) :: w →
      PathMetricBound (supportVisitPath (d i) (hd i) (hd₀ i) (f i) (hf i) (hf₀ i)
        (n * indexedWordProduct f v) d₀ r b) L κ ∧
      ∀ t, supportVisitPath (d i) (hd i) (hd₀ i) (f i) (hf i) (hf₀ i)
        (n * indexedWordProduct f v) d₀ r b t ∈ S) :
    PathMetricBound (supportWordPath d f hd hf hd₀ hf₀ d₀ r u n)
      (L * 2 ^ u.length) (κ * 2 ^ u.length) ∧
      ∀ t, supportWordPath d f hd hf hd₀ hf₀ d₀ r u n t ∈ S := by
…

Mentions: OAI.PolycyclicRecognition.PathMetricBound, OAI.PolycyclicRecognition.supportVisitPath, OAI.PolycyclicRecognition.indexedWordProduct, OAI.PolycyclicRecognition.supportWordPath

theorem OAI.PolycyclicRecognition.supportWordPath_image_bound line 84

Source documentation

Controlled images on each pair of consecutive sheets, together with the short switches between them, control the entire chosen word path.

theorem supportWordPath_image_bound
    {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (J : G → W) {K : ℝ≥0} (hJ : LipschitzWith K J)
    (u : List (I × ℝ)) (n : G) (center : W) (E : Set W)
    {B κ : ℝ} (hκ : 0 ≤ κ)
    (hbase : ∃ w ∈ E, ‖J (n * d₀) - center - r • w‖ ≤ B)
    (hsheets : ∀ (v : List (I × ℝ)) (i : I) (b : ℝ) (w : List (I × ℝ)),
      u = v ++ (i, b) :: w →
      (∀ t : unitInterval, ∃ z ∈ E,
        ‖J (((n * indexedWordProduct f v) * d₀) * d i (r * t)) -
          center - r • z‖ ≤ B) ∧
      (∀ t : unitInterval, ∃ z ∈ E,
…

Mentions: OAI.PolycyclicRecognition.indexedWordProduct