OrbitWindowMeasures.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Probability laws of finite orbit windows

A window law is the average of the actual iterated pushforwards of its initial law. For an ergodic transformation, uniformly dominated initial laws give weak convergence to the invariant probability, even for varying window lengths.

def OAI.DukePrimeDegree.orbitWindowMeasure line 25
Source documentation
N + 1 orbit samples, so the probability law is defined also at N = 0.
```
def orbitWindowMeasure (ν : Measure X) (T : X → X) (N : ℕ) : Measure X :=
…
```
lemma OAI.DukePrimeDegree.orbitWindowMeasure_univ line 29
def OAI.DukePrimeDegree.orbitWindowProbability line 40

lemma OAI.DukePrimeDegree.orbitWindowMeasure_map line 45

Source documentation

A measurable factor map commutes with the actual finite window law.

lemma orbitWindowMeasure_map {Y : Type*} [MeasurableSpace Y]
    (ν : Measure X) (S : X → X) (hS : Measurable S)
    (T : Y → Y) (hT : Measurable T) (P : X → Y) (hP : Measurable P)
    (hsem : Function.Semiconj P S T) (N : ℕ) :
    (orbitWindowMeasure ν S N).map P = orbitWindowMeasure (ν.map P) T N := by
…

Mentions: OAI.DukePrimeDegree.orbitWindowMeasure

lemma OAI.DukePrimeDegree.integral_orbitWindowMeasure line 68

theorem OAI.DukePrimeDegree.orbitWindowProbability_tendsto line 84

Source documentation

Actual orbit-window laws converge weakly. No generic-point or empirical-measure convergence premise is added.

theorem orbitWindowProbability_tendsto
    (μ : ProbabilityMeasure X) (T : X → X) (hT : Ergodic T (μ : Measure X))
    (ν : ℕ → ProbabilityMeasure X) (C : ℝ) (hC : 0 ≤ C)
    (hdom : ∀ n, (ν n : Measure X) ≤ ENNReal.ofReal C • (μ : Measure X))
    (length : ℕ → ℕ) (hlength : Tendsto length atTop atTop) :
    Tendsto (fun n => orbitWindowProbability (ν n) T
      hT.toMeasurePreserving.measurable (length n))
      atTop (𝓝 μ) := by
…

Mentions: OAI.DukePrimeDegree.orbitWindowProbability