ParametrizedSupportPaths.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Continuous sampling of prescribed generator words

When the generator indices are fixed and the amplitudes depend continuously on a parameter, every fixed time sample of the explicitly constructed path is continuous in that parameter. This retains the measurability needed for stationary endpoint averaging.

def OAI.PolycyclicRecognition.indexedWordProduct line 22
def OAI.PolycyclicRecognition.supportWordPath line 25

theorem OAI.PolycyclicRecognition.continuous_supportWordPath_sample line 34

Source documentation

Fixed-time samples of a word path are continuous under continuous variation of its amplitudes and its initial sheet.

theorem continuous_supportWordPath_sample
    {Y : Type*} [TopologicalSpace Y] (w : List (I × (Y → ℝ)))
    (hw : ∀ z ∈ w, Continuous z.2) (n : Y → G) (hn : Continuous n)
    (t : unitInterval) :
    Continuous (fun y => supportWordPath d f hd hf hd₀ hf₀ d₀ r
      (w.map (fun z => (z.1, z.2 y))) (n y) t) := by
…

Mentions: OAI.PolycyclicRecognition.supportWordPath

theorem OAI.PolycyclicRecognition.supportWordPath_bound line 61

Source documentation

The explicit word path retains the uniform metric and range bounds of its actual single-letter visits.

theorem supportWordPath_bound
    {W : Type*} [AddCommGroup W] (π : G →* Multiplicative W)
    (P : I → ℝ → Prop) (hπf : ∀ i b, P i b → π (f i b) = 1)
    {S : Set G} (hbase : ∀ n, π n = 1 → n * d₀ ∈ S)
    {L κ : ℝ} (hL : 0 ≤ L) (hκ : 0 ≤ κ)
    (hstep : ∀ n, π n = 1 → ∀ i b, P i b →
      PathMetricBound (supportVisitPath (d i) (hd i) (hd₀ i)
        (f i) (hf i) (hf₀ i) n d₀ r b) L κ ∧
      ∀ t, supportVisitPath (d i) (hd i) (hd₀ i)
        (f i) (hf i) (hf₀ i) n d₀ r b t ∈ S)
    (u : List (I × ℝ)) (hu : ∀ z ∈ u, P z.1 z.2) (n : G) (hn : π n = 1) :
    PathMetricBound (supportWordPath d f hd hf hd₀ hf₀ d₀ r u n)
…

Mentions: OAI.PolycyclicRecognition.PathMetricBound, OAI.PolycyclicRecognition.supportVisitPath, OAI.PolycyclicRecognition.supportWordPath