DiagonalProfileSampling.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A diagonal of supported laws with subexponential retained mass

Each outer parameter has its own limiting law and supported profile. The inner scale is chosen after the outer parameter, with arbitrary eventual side conditions. This preserves positive mass at every selected scale.

theorem OAI.PolycyclicRecognition.exists_diagonal_supported_neighborhoods line 18
theorem OAI.PolycyclicRecognition.exists_diagonal_good_observations line 70

theorem OAI.PolycyclicRecognition.exists_diagonal_good_profiles_on_compacts line 142

Source documentation

Choose the outer parameter and then its scale so that one diagonal is uniform on each successive compact set. Later path compacts can be absorbed by an exhaustion without making the scale depend on a particular path.

theorem exists_diagonal_good_profiles_on_compacts
    {V W A : Type*} [TopologicalSpace V] [NormedAddCommGroup W] [MeasurableSpace A]
    (S : Set C(V, W)) [MeasurableSpace S] [BorelSpace S] [HasOuterApproxClosed S]
    (K : ℕ → Set V) (hK : ∀ j, IsCompact (K j))
    (scale : ℕ → ℕ → ℝ) (hs : ∀ j, Tendsto (scale j) atTop atTop)
    (samples : ℕ → ℕ → ProbabilityMeasure A) (profile : ℕ → ℕ → A → S)
    (hp : ∀ j n, Measurable (profile j n)) (ν : ℕ → ProbabilityMeasure S)
    (hν : ∀ j, Tendsto (fun n => ProbabilityMeasure.map (samples j n) (profile j n))
      atTop (𝓝 (ν j)))
    (f : ℕ → S) (g : S) (hf : ∀ j, f j ∈ (ν j : Measure S).support)
    (hfg : Tendsto f atTop (𝓝 g))
    (P : ℕ → ℕ → Prop) (hP : ∀ j, ∀ᶠ n in atTop, P j n) :
…