Empirical measures and the Krylov–Bogolyubov theorem

This module introduces orbit empirical measures for an iterated map. This allows us to prove the Krylov–Bogolyubov (or Krylov–Bogoliubov) theorem, which asserts the existence of invariant Borel probability measures for continuous dynamics on compact metrizable spaces.

Main definitions

• empiricalMeasure: an empirical measure for n iterations of a map f starting at a point x.

Main results

• exists_measurePreserving_probabilityMeasure gives an invariant probability measure for a continuous map on a compact Hausdorff space. This is the classical Krylov-Bogolyubov theorem.
• exists_measurePreserving_probabilityMeasure_of_compact_forwardInvariant gives an invariant probability measure defined over a (not necessarily compact) ambient space, supported on a compact, forward invariant subset.

TODO

• When the Measurable requirement of MeasurePreserving is relaxed, exists_measurePreserving_probabilityMeasure_of_compact_forwardInvariant can be generalized.

noncomputable def MeasureTheory.empiricalMeasure {X : Type u_1} [MeasurableSpace X] (f : X → X) (x : X) (n : ℕ) : Measure X

An empirical measure is the Birkhoff average of the Dirac measures along an orbit starting from x under the dynamics generated by f. This uses n + 1 iterations, to give a well-defined probability measure for any n.

Equations

• MeasureTheory.empiricalMeasure f x n = birkhoffAverage NNReal f MeasureTheory.Measure.dirac (n + 1) x

instance MeasureTheory.instIsProbabilityMeasureEmpiricalMeasure {X : Type u_1} [MeasurableSpace X] (f : X → X) (x : X) (n : ℕ) : IsProbabilityMeasure (empiricalMeasure f x n)

theorem MeasureTheory.integral_empiricalMeasure_eq_birkhoffaverage {X : Type u_1} [MeasurableSpace X] (f : X → X) (x : X) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (g : X → E) [MeasurableSingletonClass X] (n : ℕ) : ∫ (y : X), g y ∂empiricalMeasure f x n = birkhoffAverage NNReal f g (n + 1) x

theorem MeasureTheory.tendsto_integral_comp_sub_integral_empiricalMeasure_of_isBoundedUnder {X : Type u_1} [MeasurableSpace X] (f : X → X) (x : X) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (g : X → E) [MeasurableSingletonClass X] (hfg : Bornology.IsBounded (Set.range fun (x_1 : ℕ) => g (f^[x_1] x))) : Filter.Tendsto (fun (n : ℕ) => ∫ (y : X), (g ∘ f) y ∂empiricalMeasure f x n - ∫ (y : X), g y ∂empiricalMeasure f x n) Filter.atTop (nhds 0)

theorem MeasureTheory.ProbabilityMeasure.integral_comp_eq_integral_of_mapClusterPt {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [BorelSpace X] {α : Type u_2} {F : Filter α} {f : X → X} (hf : Continuous f) {u : α → ProbabilityMeasure X} {μ : ProbabilityMeasure X} (hμ : MapClusterPt μ F u) {g : BoundedContinuousFunction X ℝ} (hg : Filter.Tendsto (fun (t : α) => ∫ (y : X), (⇑g ∘ f) y ∂↑(u t) - ∫ (y : X), g y ∂↑(u t)) F (nhds 0)) : ∫ (y : X), (⇑g ∘ f) y ∂↑μ = ∫ (y : X), g y ∂↑μ

If, for a bounded continuous function g, the difference between the integrals of g ∘ f and g tends to zero with respect to a filter of probability measures, then for a limit measure μ, we have ∫ y, (g ∘ f) y ∂μ = ∫ y, g y ∂μ.

theorem MeasureTheory.exists_measurePreserving_probabilityMeasure {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [BorelSpace X] [T2Space X] [CompactSpace X] [Nonempty X] {f : X → X} (hf : Continuous f) : ∃ (μ : Measure X), MeasurePreserving f μ μ ∧ μ.Regular ∧ IsProbabilityMeasure μ

Krylov-Bogolyubov theorem: there exists a regular, invariant, Borel probability measure, for a continuous function on a nonempty, compact, Hausdorff space.

theorem MeasureTheory.exists_measurePreserving_probabilityMeasure_of_compact_forwardInvariant {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [BorelSpace X] [T2Space X] {K : Set X} (hcomp : IsCompact K) (hnonempty : K.Nonempty) {f : X → X} (hfcont : ContinuousOn f K) (hfinv : Set.MapsTo f K K) (hfmeas : Measurable f) : ∃ (μ : Measure X), MeasurePreserving f μ μ ∧ μ.Regular ∧ IsProbabilityMeasure μ ∧ μ.support ⊆ K

Krylov-Bogolyubov theorem for forward invariant compact sets.