MeasurableGeneratorPrefixes.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Measurable prefixes of the fixed generator schemes

The bounded local inverse construction fixes the letter pattern. Only its real parameters vary; hence all actual prefixes and their global logarithms are measurable, including after an independently sampled initial suffix.

theorem OAI.PolycyclicRecognition.measurable_fixed_generator_word line 21

Source documentation

A fixed finite word with measurable real parameters has a measurable endpoint. This includes every prefix of a bounded generator scheme.

theorem measurable_fixed_generator_word
    {A I G : Type*} [MeasurableSpace A] [MeasurableSpace G]
    [Group G] [MeasurableMul₂ G]
    (f : I → ℝ → G) (hf : ∀ i, Measurable (f i))
    (word : List (I × (A → ℝ))) (hw : ∀ z ∈ word, Measurable z.2) :
    Measurable (fun a => (word.map (fun z => f z.1 (z.2 a))).prod) := by
…

theorem OAI.PolycyclicRecognition.measurable_fixed_generator_prefix_logs line 36

Source documentation

The actual translated logarithmic prefix is measurable. A global exponential chart provides the map log; no branch choice is involved.

theorem measurable_fixed_generator_prefix_logs
    {A I G L : Type*} [MeasurableSpace A] [MeasurableSpace G] [MeasurableSpace L]
    [Group G] [MeasurableMul₂ G]
    (f : I → ℝ → G) (hf : ∀ i, Measurable (f i))
    (word : List (I × (A → ℝ))) (hw : ∀ z ∈ word, Measurable z.2)
    (base : A → G) (hbase : Measurable base) (log : G → L) (hlog : Measurable log)
    (j : ℕ) :
    Measurable (fun a => log (base a * ((word.take j).map (fun z => f z.1 (z.2 a))).prod)) :=
…