Lumenary.ErgodicTheory

Formal library

• recurrence_pigeonholetheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Recurrence by pigeonhole.** Let `f` preserve a finite measure `μ` and let `μ(s) > 0`. Then
  some point of `s` returns to `s`. Proof: choose `N` with `N · μ(s) > μ(X)`. The sets
  `s, f⁻¹s, …, f^{-(N-1)}s` all have measure `μ(s)`, so their measures add up to more than
  `μ(X)`, and two of them meet (Mathlib's measure-theoretic pigeonhole principle
  `exists_nonempty_inter_of_measure_univ_lt_sum_measure`). If `y ∈ f^{-i}s ∩ f^{-j}s` with
  `i < j`, then `x = fⁱ(y) ∈ s` and `f^{j-i}(x) = fʲ(y) ∈ s`. -/
  theorem recurrence_pigeonhole {α : Type*} [MeasurableSpace α] {μ : Measure α}
      [IsFiniteMeasure μ] {f : α → α} (hf : MeasurePreserving f μ μ) {s : Set α}
      (hs : MeasurableSet s) (hpos : μ s ≠ 0) : ∃ x ∈ s, ∃ k, 0 < k ∧ f^[k] x ∈ s := by
    obtain ⟨N, hN⟩ := ENNReal.exists_nat_mul_gt hpos (measure_ne_top μ univ)
    have hmeas : ∀ i ∈ Finset.range N, NullMeasurableSet (f^[i] ⁻¹' s) μ :=
      fun i _ => ((hf.iterate i).measurable hs).nullMeasurableSet
    have hsum : ∑ i ∈ Finset.range N, μ (f^[i] ⁻¹' s) = N * μ s := by
      rw [Finset.sum_congr rfl fun i _ => (hf.iterate i).measure_preimage hs.nullMeasurableSet]
      simp
    obtain ⟨i, -, j, -, hij, y, hyi, hyj⟩ :=
      exists_nonempty_inter_of_measure_univ_lt_sum_measure μ hmeas (hsum ▸ hN)
    rcases lt_or_gt_of_ne hij with h | h
    · refine ⟨f^[i] y, hyi, j - i, Nat.sub_pos_of_lt h, ?_⟩
      rw [← Function.iterate_add_apply, Nat.sub_add_cancel h.le]
      exact hyj
    · refine ⟨f^[j] y, hyj, i - j, Nat.sub_pos_of_lt h, ?_⟩
      rw [← Function.iterate_add_apply, Nat.sub_add_cancel h.le]
      exact hyi

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ErgodicTheory.leanTry it in the Lean web editor

• poincare_recurrencetheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Poincaré recurrence theorem.** If `f` preserves a finite measure and `s` is measurable,
  then almost every point of `s` returns to `s` infinitely often. A measure-preserving map of a
  finite measure space is conservative (`MeasurePreserving.conservative`), and Mathlib proves
  recurrence for conservative maps (`Conservative.ae_mem_imp_frequently_image_mem`). -/
  theorem poincare_recurrence {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ]
      {f : α → α} (hf : MeasurePreserving f μ μ) {s : Set α} (hs : NullMeasurableSet s μ) :
      ∀ᵐ x ∂μ, x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s :=
    hf.conservative.ae_mem_imp_frequently_image_mem hs

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ErgodicTheory.leanTry it in the Lean web editor

• birkhoff_sum_coboundarytheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Birkhoff sums of a coboundary telescope.** If `g = h ∘ f − h`, then
  `g(x) + g(f x) + ⋯ + g(f^{n−1} x) = h(fⁿ x) − h(x)`. By induction on `n`, using Mathlib's
  `birkhoffSum_succ_apply`. -/
  theorem birkhoff_sum_coboundary {α : Type*} (f : α → α) (h : α → ℝ) (n : ℕ) (x : α) :
      birkhoffSum f (fun y => h (f y) - h y) n x = h (f^[n] x) - h x := by
    induction n with
    | zero => simp
    | succ n ih =>
      rw [birkhoffSum_succ_apply, ih, Function.iterate_succ_apply']
      ring

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ErgodicTheory.leanTry it in the Lean web editor

• coboundary_average_tendsto_zerotheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Time averages of a bounded coboundary vanish.** If `|h| ≤ C`, the Birkhoff averages of
  `h ∘ f − h` are at most `2C/n` in absolute value, so they tend to `0` at every point. In von
  Neumann's proof of the mean ergodic theorem, `L²` splits into invariant functions (where averages
  are constant) and the closure of such coboundaries (where averages tend to `0`). -/
  theorem coboundary_average_tendsto_zero {α : Type*} (f : α → α) (h : α → ℝ) {C : ℝ}
      (hC : ∀ y, |h y| ≤ C) (x : α) :
      Tendsto (fun n => birkhoffAverage ℝ f (fun y => h (f y) - h y) n x) atTop (𝓝 0) := by
    have hlim : Tendsto (fun n : ℕ => 2 * C / n) atTop (𝓝 0) :=
      tendsto_const_nhds.div_atTop tendsto_natCast_atTop_atTop
    refine squeeze_zero_norm (fun n => ?_) hlim
    rw [birkhoffAverage, birkhoff_sum_coboundary, smul_eq_mul, norm_mul, norm_inv,
      Real.norm_natCast, Real.norm_eq_abs, inv_mul_eq_div]
    gcongr
    calc |h (f^[n] x) - h x| ≤ |h (f^[n] x)| + |h x| := abs_sub _ _
      _ ≤ C + C := add_le_add (hC _) (hC _)
      _ = 2 * C := by ring

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ErgodicTheory.leanTry it in the Lean web editor

• mean_ergodictheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Von Neumann's mean ergodic theorem.** For a contraction `U` (`‖U‖ ≤ 1`) of a Hilbert space —
  for instance the Koopman operator `φ ↦ φ ∘ T` of a measure-preserving `T` on `L²(μ)` — the
  averages `(1/N) ∑_{n<N} Uⁿ x` converge in norm to the orthogonal projection of `x` onto the
  subspace of `U`-invariant vectors. This is Mathlib's
  `ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection`. -/
  theorem mean_ergodic {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
      (U : E →L[ℝ] E) (hU : ‖U‖ ≤ 1) (x : E) :
      Tendsto (birkhoffAverage ℝ U _root_.id · x) atTop
        (𝓝 ((U.eqLocus (1 : E →L[ℝ] E)).orthogonalProjectionOnto x)) :=
    U.tendsto_birkhoffAverage_orthogonalProjection hU x

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ErgodicTheory.leanTry it in the Lean web editor

• doubling_ergodictheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **The doubling map `x ↦ 2x mod 1` is ergodic** for Lebesgue (Haar) measure on the circle
  `ℝ/Tℤ`. Mathlib proves this for `x ↦ n • x` with `n ≥ 2` (`AddCircle.ergodic_nsmul`), via
  Lebesgue's density theorem. -/
  theorem doubling_ergodic (T : ℝ) [Fact (0 < T)] : Ergodic fun y : AddCircle T => 2 • y :=
    AddCircle.ergodic_nsmul (by norm_num)

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ErgodicTheory.leanTry it in the Lean web editor

• rotation_ergodic_ifftheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **A rotation of the circle `ℝ/ℤ` by `α` is ergodic iff `α` is irrational.** Mathlib shows that
  a rotation is ergodic iff the angle has infinite additive order (`AddCircle.ergodic_add_left`),
  iff its multiples are dense (`AddCircle.denseRange_zsmul_iff`), iff `α` is irrational
  (`AddCircle.denseRange_zsmul_coe_iff`). -/
  theorem rotation_ergodic_iff (α : ℝ) :
      Ergodic (fun y : AddCircle (1 : ℝ) => (α : AddCircle (1 : ℝ)) + y) ↔ Irrational α := by
    rw [AddCircle.ergodic_add_left, ← AddCircle.denseRange_zsmul_iff,
      AddCircle.denseRange_zsmul_coe_iff, div_one]

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ErgodicTheory.leanTry it in the Lean web editor