37 Dynamical systems and ergodic theory

TheoremPoincaré recurrence theorem#

Poincaré recurrence theorem: given a conservative map f and a measurable set s, almost every point x ∈ s returns back to s infinitely many times.

MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem.{u_1} {α : Type u_1} [MeasurableSpace α]
  {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.Conservative f μ)
  (hs : MeasureTheory.NullMeasurableSet s μ) :
  ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
Sources
MathlibMeasureTheory.Conservative.ae_mem_imp_frequently_image_mem
Uses 7
Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Carathéodory's theorem (measure theory) · Linear map · Measurable function · Positive measure
Proof usesOrdered ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.