OccupationLimitSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Selecting one occupation limit while preserving the profile limit

theorem OAI.PolycyclicRecognition.exists_occupation_limit_preserving line 17

Source documentation

Compactness selects a single occupation limit on a finer filter, and every already established profile limit is retained. The filter and the occupation measure are selected before any microstep length.

theorem exists_occupation_limit_preserving
    {X Y ι : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y]
    {l : Filter ι} [l.NeBot] (μs : ι → ProbabilityMeasure X)
    {profiles : ι → Y} {ν : Y} (hν : Tendsto profiles l (𝓝 ν)) :
    ∃ (u : Ultrafilter ι) (μ : ProbabilityMeasure X),
      (u : Filter ι) ≤ l ∧ Tendsto μs u (𝓝 μ) ∧ Tendsto profiles u (𝓝 ν) := by
…

theorem OAI.PolycyclicRecognition.integral_tendsto_zero_of_lintegral_nonneg line 31

Source documentation

The stationary nonnegative integral is the real integral used by the microstep estimate, so convergence of the former supplies the latter.

theorem integral_tendsto_zero_of_lintegral_nonneg
    {X ι : Type*} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
    (μ : Measure X) {l : Filter ι} (f : ι → C(X, ℝ))
    (hp : ∀ i x, 0 ≤ f i x)
    (hlim : Tendsto (fun i => ∫⁻ x, ENNReal.ofReal (f i x) ∂μ) l (𝓝 0)) :
    Tendsto (fun i => ∫ x, f i x ∂μ) l (𝓝 0) := by
…