OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportVisitRescale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.supportVisitPath_comp_mul line 15

   Source documentation

   Rescaling the root subgroup parameter preserves every point of the outward-switch-return path, including its parametrization.

   theorem supportVisitPath_comp_mul
       (d : ℝ → G) (hd : Continuous d) (hd₀ : d 0 = 1)
       (f : ℝ → G) (hf : Continuous f) (hf₀ : f 0 = 1)
       (n d₀ : G) (r b a : ℝ) (t : unitInterval) :
       supportVisitPath d hd hd₀ (fun u => f (u * a))
         (hf.comp (continuous_id.mul_const a)) (by simpa using hf₀) n d₀ r b t =
       supportVisitPath d hd hd₀ f hf hf₀ n d₀ r (b * a) t := by
   …

   Mentions: OAI.PolycyclicRecognition.supportVisitPath

2. theorem OAI.PolycyclicRecognition.supportVisitPath_comp_mul_metric line 27

   Source documentation

   The exact reparametrization transports the coarse metric estimate.

   theorem supportVisitPath_comp_mul_metric
       (d : ℝ → G) (hd : Continuous d) (hd₀ : d 0 = 1)
       (f : ℝ → G) (hf : Continuous f) (hf₀ : f 0 = 1)
       (n d₀ : G) (r b a L κ : ℝ)
       (h : PathMetricBound (supportVisitPath d hd hd₀ f hf hf₀ n d₀ r (b * a)) L κ) :
       PathMetricBound (supportVisitPath d hd hd₀ (fun u => f (u * a))
         (hf.comp (continuous_id.mul_const a)) (by simpa using hf₀) n d₀ r b) L κ := by
   …

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