SupportVisitPaths.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Outward, switch, and return paths

The actual three curves are concatenated, retaining their exact heights and the logarithmic switch error. This statement is independent of how the switch estimate is obtained and is used below for the Cartan root curves.

def OAI.PolycyclicRecognition.flowPath line 22

def OAI.PolycyclicRecognition.supportVisitPath line 30

Source documentation

The specified outward-switch-return path, with no choice of curves.

def supportVisitPath (d : ℝ → G) (hd : Continuous d) (hzero : d 0 = 1)
    (f : ℝ → G) (hf : Continuous f) (hf₀ : f 0 = 1) (n d₀ : G) (r b : ℝ) :
    Path (n * d₀) (n * f b * d₀) :=
…

theorem OAI.PolycyclicRecognition.supportVisitPath_apply_congr line 45

Source documentation

Pointwise changes of representation preserve the specified visit curve.

theorem supportVisitPath_apply_congr
    (d d' f f' : ℝ → G) (hd : Continuous d) (hd' : Continuous d')
    (hd₀ : d 0 = 1) (hd₀' : d' 0 = 1)
    (hf : Continuous f) (hf' : Continuous f') (hf₀ : f 0 = 1) (hf₀' : f' 0 = 1)
    (he_d : ∀ t, d t = d' t) (he_f : ∀ t, f t = f' t)
    (n k k' : G) (he_k : k = k') (r b : ℝ) (t : unitInterval) :
    supportVisitPath d hd hd₀ f hf hf₀ n k r b t =
      supportVisitPath d' hd' hd₀' f' hf' hf₀' n k' r b t := by
…

Mentions: OAI.PolycyclicRecognition.supportVisitPath

theorem OAI.PolycyclicRecognition.continuous_supportVisitPath_sample line 61

Source documentation

Every fixed time sample depends continuously on the initial sheet and the switch amplitude.

theorem continuous_supportVisitPath_sample
    (d : ℝ → G) (hd : Continuous d) (hzero : d 0 = 1)
    (f : ℝ → G) (hf : Continuous f) (hf₀ : f 0 = 1)
    {Y : Type*} [TopologicalSpace Y] (n : Y → G) (hn : Continuous n)
    (b : Y → ℝ) (hb : Continuous b) (d₀ : G) (r : ℝ) (t : unitInterval) :
    Continuous (fun y => supportVisitPath d hd hzero f hf hf₀ (n y) d₀ r (b y) t) := by
…

Mentions: OAI.PolycyclicRecognition.supportVisitPath

theorem OAI.PolycyclicRecognition.supportVisitPath_uniform_bound line 89

Source documentation

Concatenate a support leg, a height-zero switch, and the reverse leg. The constants are uniform over both the translated sheet and the pivot.

theorem supportVisitPath_uniform_bound
    (π : G →* Multiplicative W) (d : ℝ → G) (hd : Continuous d) (hzero : d 0 = 1)
    (hmul : ∀ s t, d (s + t) = d s * d t)
    {E : Set W} (hE : Convex ℝ E) {w₀ w₁ : W} (hw₀ : w₀ ∈ E) (hw₁ : w₁ ∈ E)
    (hπd : ∀ t, (π (d t)).toAdd = t • (w₁ - w₀)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (r : ℝ), 0 ≤ r → ∀ (n d₀ : G),
      π n = 1 → (π d₀).toAdd = r • w₀ →
      ∀ (f : ℝ → G) (hf : Continuous f) (hf₀ : f 0 = 1), (∀ t, π (f t) = 1) →
      ∀ (b κ : ℝ), 0 ≤ κ →
      (∀ s ∈ Set.Icc (0 : ℝ) 1, ∀ t ∈ Set.Icc (0 : ℝ) 1,
        dist (n * f (s * b) * (d₀ * d r)) (n * f (t * b) * (d₀ * d r)) ≤ κ) →
      PathMetricBound (supportVisitPath d hd hzero f hf hf₀ n d₀ r b)
…

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

theorem OAI.PolycyclicRecognition.exists_support_visit_path_bound line 162

Source documentation

The explicit visit path also supplies the existential interface.

theorem exists_support_visit_path_bound
    (π : G →* Multiplicative W) (d : ℝ → G) (hd : Continuous d) (hzero : d 0 = 1)
    (hmul : ∀ s t, d (s + t) = d s * d t)
    {E : Set W} (hE : Convex ℝ E) {w₀ w₁ : W} (hw₀ : w₀ ∈ E) (hw₁ : w₁ ∈ E)
    (hπd : ∀ t, (π (d t)).toAdd = t • (w₁ - w₀)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (r : ℝ), 0 ≤ r → ∀ (n d₀ : G),
      π n = 1 → (π d₀).toAdd = r • w₀ →
      ∀ (f : ℝ → G), Continuous f → f 0 = 1 → (∀ t, π (f t) = 1) →
      ∀ (b κ : ℝ), 0 ≤ κ →
      (∀ s ∈ Set.Icc (0 : ℝ) 1, ∀ t ∈ Set.Icc (0 : ℝ) 1,
        dist (n * f (s * b) * (d₀ * d r)) (n * f (t * b) * (d₀ * d r)) ≤ κ) →
      ∃ p : Path (n * d₀) (n * f b * d₀),
…