OAI/GroupTheory/PolycyclicRecognition/Analysis/ReachableTuplePaths.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.reachable_image_tuple_paths line 20

   Source documentation

   Successful parameters may be correlated. Only their actual reachable states and paths are used when constructing all image-tuple transitions.

   theorem reachable_image_tuple_paths
       {h : ℕ} (ι : N →* G) (f : G → G) {Λ : ℝ≥0} (hf : LipschitzWith Λ f)
       (π : G →* Multiplicative W) (x d : G) (initial : N)
       (S : Set (Fin h → N)) (P : T → Prop) (boundary : T → ℕ → N)
       (hzero : ∀ t, P t → boundary t 0 = initial)
       (hreach : ∀ v ∈ S, ∃ t, P t ∧ ∀ i : Fin h, boundary t (i.val + 1) = v i)
       (E : Fin h → Set W) (r L κ B D : ℝ)
       (hpaths : ∀ t, P t → ∀ j : Fin h,
         ∃ γ : Path (x * ι (boundary t j.val) * d) (x * ι (boundary t (j.val + 1)) * d),
           PathMetricBound γ L κ ∧
           (∀ u, ∃ w ∈ E j, ‖(π (f (γ u))).toAdd -
             (π (f (x * ι (boundary t j.val) * d))).toAdd - r • w‖ ≤ B) ∧
   …

   Mentions: OAI.PolycyclicRecognition.PathMetricBound

2. theorem OAI.PolycyclicRecognition.source_bundle_image_tuple_paths line 66

   Source documentation

   Apply the transfer directly to the source-state coordinates produced by the coupled Haar image theorem. No independent choice of increments or of their conjugated images is made.

   theorem source_bundle_image_tuple_paths
       {h : ℕ} (ι : N →* G) (f : G → G) {Λ : ℝ≥0} (hf : LipschitzWith Λ f)
       (π : G →* Multiplicative W) (x d : G) (initial : N)
       (S : Set (Fin h → N)) (P : T → Prop) (products : T → Fin h → N)
       (φ : Fin h → N ≃* N) (ψ : Fin h → N ≃ᵐ N) (hψ : ∀ i z, ψ i z = φ i z)
       (hreach : ∀ v ∈ S, ∃ t, P t ∧ v = sourceBundleStateEquiv h initial ψ (products t))
       (E : Fin h → Set W) (r L κ B D : ℝ)
       (hpaths : ∀ t, P t → ∀ j : Fin h,
         ∃ γ : Path (x * ι (sourceBundleBoundary initial φ (products t) j.val) * d)
             (x * ι (sourceBundleBoundary initial φ (products t) (j.val + 1)) * d),
           PathMetricBound γ L κ ∧
           (∀ u, ∃ w ∈ E j, ‖(π (f (γ u))).toAdd -
   …

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