SupportVisitImage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Image control on a visit between two good sheets

Only the outward and return sheets require a prescribed profile. The short root switch is controlled from its first endpoint by Lipschitz continuity.

theorem OAI.PolycyclicRecognition.supportVisitPath_metric_bound line 23

Source documentation

The metric estimate for the actual visit does not require any height homomorphism or restriction on the initial sheet.

theorem supportVisitPath_metric_bound
    (d : ℝ → G) (hd : Continuous d) (hzero : d 0 = 1)
    (hmul : ∀ s t, d (s + t) = d s * d t) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ r : ℝ, 0 ≤ r → ∀ n d₀ : G,
      ∀ (f : ℝ → G) (hf : Continuous f) (hf₀ : f 0 = 1) (b κ : ℝ), 0 ≤ κ →
      (∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ 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)
        (4 * C * r) (4 * (C + κ)) := by
…

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

theorem OAI.PolycyclicRecognition.supportVisitPath_image_bound line 65

Source documentation

An arbitrary Lipschitz observable has controlled image on the whole visit once both endpoint sheets have controlled images along the support leg.

theorem supportVisitPath_image_bound
    (d : ℝ → G) (hd : Continuous d) (hzero : d 0 = 1)
    (f : ℝ → G) (hf : Continuous f) (hf₀ : f 0 = 1)
    (J : G → W) {K : ℝ≥0} (hJ : LipschitzWith K J)
    (n d₀ : G) (r b : ℝ) (center : W) (E : Set W) {B κ : ℝ}
    (hκ : 0 ≤ κ)
    (hout : ∀ t : unitInterval, ∃ w ∈ E,
      ‖J ((n * d₀) * d (r * t)) - center - r • w‖ ≤ B)
    (hback : ∀ t : unitInterval, ∃ w ∈ E,
      ‖J ((n * f b * d₀) * d (r * t)) - center - r • w‖ ≤ B)
    (hswitch : ∀ t : unitInterval,
      dist (n * f ((t : ℝ) * b) * (d₀ * d r)) ((n * d₀) * d r) ≤ κ) :
…