SequenceCellProfiles.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Good profiles in the original Haar cells

The good sets remain subsets of the original recurrence cells, and their probability estimate is exactly a relative Haar-volume estimate.

theorem OAI.PolycyclicRecognition.cellProbabilityMeasure_apply_toReal line 19

theorem OAI.PolycyclicRecognition.exists_good_cell_profiles_sequence line 31

Source documentation

The supported profile law gives shrinking errors on a prescribed compact set and good subsets of the actual recurrence cells with relative mass at least exp(-o(scale)).

theorem exists_good_cell_profiles_sequence
    {V W N : Type*} [TopologicalSpace V] [NormedAddCommGroup W] [MeasurableSpace N]
    (S : Set C(V, W)) [MeasurableSpace S] [BorelSpace S] [HasOuterApproxClosed S]
    (K : Set V) (hK : IsCompact K)
    (scale : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (μ : Measure N) (Q : ℕ → Set N) (hQ : ∀ n, MeasurableSet (Q n))
    (hQ0 : ∀ n, μ (Q n) ≠ 0) (hQfin : ∀ n, μ (Q n) ≠ ∞)
    (profile : ℕ → N → S) (hp : ∀ n, Measurable (profile n))
    (ν : ProbabilityMeasure S)
    (hν : Tendsto (fun n => ProbabilityMeasure.map
      (cellProbabilityMeasure μ (Q n) (hQ0 n) (hQfin n)) (profile n)) atTop (𝓝 ν))
    {f : S} (hf : f ∈ (ν : Measure S).support) :
…

Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure