OAI/GroupTheory/PolycyclicRecognition/Geometry/SupportFlowLegs.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual one-parameter legs between support positions

The height along a translated one-parameter leg is the affine segment between its endpoint heights. Its metric bound is uniform at scale r, with one fixed additive constant for the finite-mesh argument.

  1. def OAI.PolycyclicRecognition.flowLeg line 20
  2. theorem OAI.PolycyclicRecognition.flowLeg_endpoints line 23
  3. theorem OAI.PolycyclicRecognition.exists_flowLeg_coarse_bound line 27
  4. theorem OAI.PolycyclicRecognition.flowLeg_height line 40
  5. theorem OAI.PolycyclicRecognition.flowLeg_height_mem line 51

    Source documentation

    Convexity keeps every height on the leg inside the scaled template.

    theorem flowLeg_height_mem (π : G →* Multiplicative W) (d : ℝ → G)
    {E : Set W} (hE : Convex ℝ E) {w₀ w₁ : W} (hw₀ : w₀ ∈ E) (hw₁ : w₁ ∈ E)
    (hd : ∀ t, (π (d t)).toAdd = t • (w₁ - w₀))
    {x : G} {r : ℝ} (hx : (π x).toAdd = r • w₀) {t : ℝ}
    (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    ∃ w ∈ E, (π (flowLeg d x r t)).toAdd = r • w := by
…

    Mentions: OAI.PolycyclicRecognition.flowLeg