ProfileChainConcentration.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Propagating a profile through a bounded number of interior switches

The individual switch theorem is applied to marginal laws. Compactness then gives joint concentration of every intermediate profile near the initial one. The number of switches is fixed; no simultaneous success assumption about all probes is needed.

theorem OAI.PolycyclicRecognition.profile_chain_concentration line 26

Source documentation

Equality of all adjacent marginal limits propagates through the whole finite chain, on the actual compact set of profile coordinates.

theorem profile_chain_concentration
    (S : Set C(V, W)) [CompactSpace S] [MetrizableSpace S]
    [MeasurableSpace S] [BorelSpace S]
    (Z : Set V) [CompactSpace Z] (n : ℕ)
    (μ : ℕ → ProbabilityMeasure (Fin (n + 1) → S))
    (hedge : ∀ i : Fin n, ∀ ι : ℕ → ℕ, StrictMono ι →
      ∀ ν : ProbabilityMeasure (S × S),
      Tendsto (fun k => ProbabilityMeasure.map (μ (ι k))
        (fun f => (f i.castSucc, f i.succ))) atTop (𝓝 ν) →
      ∀ f ∈ (ν : Measure (S × S)).support, ∀ z ∈ Z, f.1.val z = f.2.val z)
    (j : Fin (n + 1)) {η : ℝ} (hη : 0 < η) :
    Tendsto (fun k => (μ k : Measure (Fin (n + 1) → S))
…

theorem OAI.PolycyclicRecognition.independent_profile_chain_concentration line 69

Source documentation

The finite-chain conclusion survives arbitrary independent probe laws. Only adjacent deterministic marginal limits have to be identified.

theorem independent_profile_chain_concentration
    (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))
    (hedge : ∀ k : ∀ m, K m, ∀ i : Fin n, ∀ ι : ℕ → ℕ, StrictMono ι →
      ∀ limitLaw : ProbabilityMeasure (S × S),
      Tendsto (fun m => ProbabilityMeasure.map
…