OAI/GroupTheory/PolycyclicRecognition/Geometry/CoarseFlowBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform coarse bounds along actual one-parameter subgroups

Continuity and the homomorphism law suffice for the path-mesh estimates. The additive constant accommodates short parameter intervals without an extra Riemannian regularity assumption on the ambient metric.

  1. theorem OAI.PolycyclicRecognition.continuous_flow_coarse_bound line 20
  2. theorem OAI.PolycyclicRecognition.continuous_flow_coarse_dist line 53

    Source documentation

    Differences along the flow have the same uniform bound.

    theorem continuous_flow_coarse_dist (d : ℝ → G) (hd : Continuous d) (hzero : d 0 = 1)
    (hmul : ∀ s t, d (s + t) = d s * d t) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ s t : ℝ, dist (d s) (d t) ≤ C * (1 + |t - s|) := by
…