InvariantMeasure.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.CompactInvariant.iterateLaw line 15
Source documentation
The pushforward of the initial probability by the jth iterate.
```
noncomputable def iterateLaw (T : X → X) (hT : Continuous T)
    (μ : ProbabilityMeasure X) (j : ℕ) : ProbabilityMeasure X :=
…
```
def OAI.SmoothObstruction.CompactInvariant.cesaro line 23
Source documentation
Cesaro averages indexed by n+1 to keep the total mass equal to one even at the first index. No ergodic theorem is used in their construction.
```
noncomputable def cesaro (T : X → X) (hT : Continuous T)
    (μ : ProbabilityMeasure X) (n : ℕ) : ProbabilityMeasure X :=
…
```
lemma OAI.SmoothObstruction.CompactInvariant.integral_iterateLaw line 32
lemma OAI.SmoothObstruction.CompactInvariant.integral_cesaro line 37
lemma OAI.SmoothObstruction.CompactInvariant.cesaro_integral_defect line 45
lemma OAI.SmoothObstruction.CompactInvariant.integral_iterate_bound line 62
lemma OAI.SmoothObstruction.CompactInvariant.cesaro_integral_defect_bound line 70
lemma OAI.SmoothObstruction.CompactInvariant.cesaro_integral_defect_tendsto line 83

theorem OAI.SmoothObstruction.CompactInvariant.cesaro_limit_invariant line 96

Source documentation

Any weak limit of the Cesaro orbit averages is invariant.

theorem cesaro_limit_invariant (T : X → X) (hT : Continuous T)
    (μ ν : ProbabilityMeasure X) {φ : ℕ → ℕ} (hφ : Tendsto φ atTop atTop)
    (hlim : Tendsto ((cesaro T hT μ) ∘ φ) atTop (𝓝 ν)) :
    MeasurePreserving T (ν : Measure X) (ν : Measure X) := by
…

Mentions: OAI.SmoothObstruction.CompactInvariant.cesaro

theorem OAI.SmoothObstruction.CompactInvariant.exists_invariant_probability line 117
Source documentation
Compactness of probability measures provides a genuine invariant law. This is the Krylov--Bogoliubov argument used twice in the manuscript.
```
theorem exists_invariant_probability [Nonempty X] (T : X → X) (hT : Continuous T) :
    ∃ μ : ProbabilityMeasure X, MeasurePreserving T (μ : Measure X) (μ : Measure X) := by
…
```
def OAI.SmoothObstruction.CompactInvariant.testEmbedding line 127
Source documentation
Real continuous test integrals embed probability laws into a locally convex product space. This permits direct reuse of Mathlib's Krein--Milman lemma, without an unproved ergodic-decomposition input.
```
noncomputable def testEmbedding (μ : ProbabilityMeasure X) : (X →ᵇ ℝ) → ℝ :=
…
```
lemma OAI.SmoothObstruction.CompactInvariant.continuous_testEmbedding line 131
lemma OAI.SmoothObstruction.CompactInvariant.testEmbedding_injective line 137
lemma OAI.SmoothObstruction.CompactInvariant.invariant_probabilities_closed line 145
theorem OAI.SmoothObstruction.CompactInvariant.exists_ergodic_probability line 155
Source documentation
Every continuous self-map of a nonempty compact metrizable Borel space has an ergodic invariant probability law, obtained as an extreme point.
```
theorem exists_ergodic_probability [Nonempty X] (T : X → X) (hT : Continuous T) :
    ∃ μ : ProbabilityMeasure X, Ergodic T (μ : Measure X) := by
…
```
theorem OAI.SmoothObstruction.CompactInvariant.exists_probability_lift line 200
Source documentation
Probability measures lift through continuous surjections from a compact metric space. Finite simple approximants avoid any selection assumption.
```
theorem exists_probability_lift (π : X → Y) (hπ : Continuous π)
    (hsur : Function.Surjective π) (μ : ProbabilityMeasure Y) :
    ∃ ν : ProbabilityMeasure X, (ν : Measure X).map π=(μ : Measure Y) := by
…
```

theorem OAI.SmoothObstruction.CompactInvariant.exists_invariant_lift line 246

Source documentation

The required stationary lift with exactly the prescribed marginal. This uses compactness and actual finite probability approximants, not a chosen stationary lift as an additional hypothesis.

theorem exists_invariant_lift (π : X → Y) (hπ : Continuous π)
    (hsur : Function.Surjective π) (T : X → X) (hT : Continuous T) (S : Y → Y)
    (hsem : Function.Semiconj π T S) (μ : ProbabilityMeasure Y)
    (hS : MeasurePreserving S (μ : Measure Y) (μ : Measure Y)) :
    ∃ ν : ProbabilityMeasure X, MeasurePreserving T (ν : Measure X) (ν : Measure X) ∧
      (ν : Measure X).map π=(μ : Measure Y) := by
…