OccupationFlowLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Convex flow increments from dominated occupation laws

theorem OAI.PolycyclicRecognition.normalized_flow_error_tendsto_zero line 22

Source documentation

For a genuine continuous one-parameter subgroup all mesh, remainder, and endpoint hypotheses follow from the flow laws. Only the occupation comparison and the stationary estimate remain to be supplied.

theorem normalized_flow_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 (𝓝 μ))
    (d : ℝ → G) (hd : Continuous d) (hd0 : d 0 = 1)
    (hmul : ∀ s t, d (s + t) = d s * d t)
    (t : ι → ℝ) (ht : Tendsto t l atTop) (c : ℝ≥0)
    (hdom : ∀ L : ℕ, 0 < L → ∀ᶠ i in l, ∀ j : Fin ⌊t i / (L : ℝ)⌋₊,
      Measure.map (fun p : NormalizedPair G Λ => (d L ^ (j : ℕ))⁻¹ • p)
        (σ i : Measure _) ≤ c • (μs i : Measure _))
    {S : Set W} (hS : IsCompact S) {w₀ : W} (hw₀ : w₀ ∈ S)
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair