OAI/GroupTheory/PolycyclicRecognition/Geometry/OccupationFlowMicrosteps.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact microstep decomposition of a continuous one-parameter subgroup

  1. theorem OAI.PolycyclicRecognition.exists_flow_microstep_bound line 19

    Source documentation

    A fixed integer microstep leaves a remainder of uniformly bounded length. The endpoint factorization is exact.

    theorem exists_flow_microstep_bound (d : ℝ → G) (hd : Continuous d)
    (hd0 : d 0 = 1) (hmul : ∀ s t, d (s + t) = d s * d t) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ L : ℕ, 0 < L → ∀ t : ℝ, 0 < t →
      let n := ⌊t / (L : ℝ)⌋₊
…