OAI/GroupTheory/PolycyclicRecognition/Algebra/SuccessfulSourceWord.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.successful_sourceBundle_word_good line 21

   Source documentation

   Each global successful parameter gives exactly the good word needed by the profile path construction on its own bundle sheet.

   theorem successful_sourceBundle_word_good {h m : ℕ}
       (lie : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) N)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) N → N)
       (X : I → L) (s : I → ℝ) (letters : Fin m → I) (r : ℝ)
       (φ : Fin h → N ≃* N) (sample : ℕ → ℝ → N)
       (hsub : ∀ j u v, sample j u * (sample j v)⁻¹ = sample j (u - v))
       (hsample : ∀ (i : Fin h) (j : Fin m) t,
         sample (finProdFinEquiv (i, j)).val t = φ i
           (Exp (lie (t • (Real.exp (r * s (letters j)) • X (letters j))))))
       (Good : Set N) (initial : N) (hi : initial ∈ Good)
       (t : Fin (h * m + h * m) → ℝ)
       (hs : SwitchSuccessful (fun _ => Good) 0 (h * m) initial
   …

   Mentions: OAI.PolycyclicRecognition.SwitchSuccessful