OAI/GroupTheory/PolycyclicRecognition/Analysis/SourceBundleTerminalPaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_source_bundle_terminal_path line 21

   Source documentation

   All source bundle boundaries have the same height. Their common template therefore survives concatenation without a sum of templates.

   theorem exists_source_bundle_terminal_path
       (ι : N →* G) (π : G →* Multiplicative W) (hN : ∀ n, π (ι n) = 1)
       {h : ℕ} (initial : N) (φ : Fin h → N ≃* N) (products : Fin h → N)
       (x d : G) (E : Set W) (hE0 : (0 : W) ∈ E)
       (r L κ B : ℝ) (hL : 0 ≤ L) (hκ : 0 ≤ κ) (hB : 0 ≤ B)
       (path : ∀ j : Fin h,
         Path (x * ι (sourceBundleBoundary initial φ products j.val) * d)
           (x * ι (sourceBundleBoundary initial φ products (j.val + 1)) * d))
       (hmetric : ∀ j, PathMetricBound (path j) L κ)
       (hheight : ∀ j t, ∃ w ∈ E,
         ‖(π (path j t)).toAdd -
             (π (x * ι (sourceBundleBoundary initial φ products j.val) * d)).toAdd -
   …

   Mentions: OAI.PolycyclicRecognition.sourceBundleBoundary, OAI.PolycyclicRecognition.PathMetricBound