OAI/NumberTheory/DukePrimeDegree/Dynamics/OrbitRecurrence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Recurrence with close orbit parameters

For the exceptional-return argument, recurrence is needed in the parameter topology of an orbit, which need not be closed in the ambient quotient. A countable cover by compact parameter neighborhoods makes their images measurable, and ordinary Poincaré recurrence supplies the required return.

  1. lemma OAI.DukePrimeDegree.exists_compact_close_parameter_neighborhood line 28
  2. theorem OAI.DukePrimeDegree.exists_close_parameters_of_orbit_recurrence line 41

    Source documentation

    Poincaré recurrence in the topology of orbit parameters. This does not require the orbit image to be closed or its inverse parametrization continuous.

    theorem exists_close_parameters_of_orbit_recurrence
    (μ : Measure X) [IsFiniteMeasure μ] [NeZero μ]
    (f : X → X) (hf : MeasurePreserving f μ μ)
    (ψ : G → X) (hψ : Continuous ψ) (hfull : ∀ᵐ x ∂μ, x ∈ range ψ)
    (U : Set G) (hU : U ∈ 𝓝 1) (N : ℕ) :
    ∃ n > N, ∃ a b : G, a⁻¹ * b ∈ U ∧ f^[n] (ψ a) = ψ b := by
…