OccupationMicrostepLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The two successive limits in the convex increment argument

theorem OAI.PolycyclicRecognition.normalized_microstep_error_tendsto_zero line 23

Source documentation

First take the chart scale to infinity for a fixed integer microstep, then take the microstep length to infinity for the single limiting law. No rate of stationary convergence uniform over probabilities is used.

theorem normalized_microstep_error_tendsto_zero
    {ι : Type*} {l : Filter ι}
    (π : G →* Multiplicative W) (hπ : LipschitzWith K (fun g => (π g).toAdd))
    (σ μs : ι → ProbabilityMeasure (NormalizedPair G Λ))
    (μ : ProbabilityMeasure (NormalizedPair G Λ))
    (hμ : Tendsto μs l (𝓝 μ))
    (t : ι → ℝ) (ht : Tendsto t l atTop)
    (endpoint : ι → G) (g : ℕ → G) (n : ℕ → ι → ℕ) (h : ℕ → ι → G)
    (c : ℝ≥0) {D : ℝ} (hD : 0 ≤ D)
    (hsteps : ∀ L : ℕ, 0 < L → ∀ᶠ r in l,
      0 < t r ∧ (n L r : ℝ) * L ≤ t r ∧ t r ≤ ((n L r : ℝ) + 1) * L ∧
      dist 1 (h L r) ≤ D * L ∧ g L ^ n L r * h L r = endpoint r ∧
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair