FiniteModeProfileChains.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite generator choices in the independent profile chains

theorem OAI.PolycyclicRecognition.exists_constant_mode_subsequence line 16
Source documentation
Along a further increasing subsequence a finite generator index is constant. This leaves an already converging profile law unchanged.
```
theorem exists_constant_mode_subsequence {I : Type*} [Finite I] (mode : ℕ → I) :
    ∃ i : I, ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, mode (φ n) = i := by
…
```

theorem OAI.PolycyclicRecognition.independent_profile_chain_concentration_finite_modes line 30

Source documentation

The selected word may use a different finite generator at every scale. It suffices to verify each actual fixed-generator subsequence.

theorem independent_profile_chain_concentration_finite_modes
    {V W I : Type*} [TopologicalSpace V] [NormedAddCommGroup W] [Finite I]
    (S : Set C(V, W)) [CompactSpace S] [MetrizableSpace S]
    [MeasurableSpace S] [BorelSpace S]
    (Z : Set V) [CompactSpace Z] (n : ℕ)
    {A K : ℕ → Type*} [∀ m, MeasurableSpace (A m)] [∀ m, MeasurableSpace (K m)]
    [∀ m, Nonempty (K m)]
    (μ : ∀ m, ProbabilityMeasure (A m)) (ν : ∀ m, ProbabilityMeasure (K m))
    (profile : ∀ m, A m × K m → Fin (n + 1) → S)
    (hp : ∀ m, Measurable (profile m))
    (mode : ∀ m, K m → Fin n → I)
    (hedge : ∀ k : ∀ m, K m, ∀ edge : Fin n, ∀ i : I,
…