OAI/GroupTheory/PolycyclicRecognition/Analysis/MeasurableGeneratorChain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_measurable_generator_chain line 12

   Source documentation

   Padding uses a fixed zero letter. The selected letter pattern is independent of the sampled endpoint, and every prefix is measurable.

   theorem exists_measurable_generator_chain
       {A I L G : Type*} [MeasurableSpace A] [MeasurableSpace G]
       [AddCommMonoid L] [Module ℝ L] [Group G] [MeasurableMul₂ G]
       (X : I → L) (Exp : L → G) (hzero : Exp 0 = 1)
       (hf : ∀ i, Measurable (fun t : ℝ => Exp (t • X i)))
       (i₀ : I) (word : List (I × (A → ℝ)))
       (hw : ∀ z ∈ word, Measurable z.2)
       {N : ℕ} (hlen : word.length ≤ N) {C : ℝ} (hC : 0 ≤ C)
       (hamp : ∀ a, ∀ z ∈ word, |z.2 a| ≤ C)
       (base : A → G) (hbase : Measurable base) :
       ∃ (mode : Fin N → I) (coeff : A → Fin N → ℝ)
         (vertex : A → Fin (N + 1) → G),
   …