ParametrizedGeneratorSchemes.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Continuous path samples for the finite generator schemes

The conjugating letters are fixed. Only the inserted amplitudes vary, so the whole expanded word has a fixed combinatorial pattern and continuous amplitudes. This makes each of its support-path samples continuous.

def OAI.PolycyclicRecognition.parameterGeneratorSchemeWord line 19
theorem OAI.PolycyclicRecognition.parameterGeneratorSchemeWord_eval line 26
theorem OAI.PolycyclicRecognition.parameterGeneratorSchemeWord_continuous line 35

theorem OAI.PolycyclicRecognition.continuous_generatorScheme_path_sample line 59

Source documentation

Evaluating a chosen finite scheme through continuous local inverse coordinates gives continuous, hence Borel, fixed-time path samples.

theorem continuous_generatorScheme_path_sample
    (w : Fin k → List (I × ℝ)) (i : Fin k → I)
    (σ : Y → Fin k → ℝ) (hσ : Continuous σ)
    (n : Y → G) (hn : Continuous n) (d₀ : G) (r : ℝ) (t : unitInterval) :
    Continuous (fun y => supportWordPath d f hd hf hd₀ hf₀ d₀ r
      (generatorSchemeWord w i (σ y)) (n y) t) := by
…

Mentions: OAI.PolycyclicRecognition.supportWordPath, OAI.PolycyclicRecognition.generatorSchemeWord