SuccessfulSamplePaths.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact path endpoint of a successful sample sequence

theorem OAI.PolycyclicRecognition.WordSheetsGood.map_mul_hom line 16
Source documentation
Transport the visited sheets through a subgroup map and a fixed left translate.
```
theorem WordSheetsGood.map_mul_hom (ι : N →* G) (x : G)
    {A : Set N} {n : N} {u : List N} (h : WordSheetsGood A n u) :
    WordSheetsGood ((fun v => x * ι v) '' A) (x * ι n) (u.map ι) := by
…
```
Mentions: OAI.PolycyclicRecognition.WordSheetsGood

theorem OAI.PolycyclicRecognition.successful_sample_path line 30

Source documentation

A successful independent sample sequence gives the specified geometric word path to its actual group endpoint, with bounds inherited from its single-letter visits on the good sheets.

theorem successful_sample_path
    (ι : N →* G) (x d₀ : G) (A : Set N) (S : Set G) (m : ℕ)
    (sample : ℕ → ℝ → N) (hsub : ∀ j s t, sample j s * (sample j t)⁻¹ = sample j (s - t))
    (d : Fin m → ℝ → G) (hd : ∀ i, Continuous (d i)) (hd₀ : ∀ i, d i 0 = 1)
    (hf : ∀ i : Fin m, Continuous (fun t => ι (sample i.val t)))
    (hf₀ : ∀ i : Fin m, ι (sample i.val 0) = 1)
    (r : ℝ) {L κ ρ : ℝ} (hL : 0 ≤ L) (hκ : 0 ≤ κ)
    (hbase : ∀ n ∈ A, x * ι n * d₀ ∈ S)
    (hstep : ∀ n ∈ A, ∀ i : Fin m, ∀ b : ℝ, |b| ≤ 2 * ρ → n * sample i.val b ∈ A →
      PathMetricBound (supportVisitPath (d i) (hd i) (hd₀ i)
        (fun t => ι (sample i.val t)) (hf i) (hf₀ i) (x * ι n) d₀ r b) L κ ∧
      ∀ t, supportVisitPath (d i) (hd i) (hd₀ i)
…

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