feat(Dynamics/Birkhoff): define Birkhoff sum and Birkhoff average (#6131

)

Mathlib.lean

@@ -1834,6 +1834,8 @@ import Mathlib.Deprecated.Subfield
 import Mathlib.Deprecated.Subgroup
 import Mathlib.Deprecated.Submonoid
 import Mathlib.Deprecated.Subring
+import Mathlib.Dynamics.BirkhoffSum.Average
+import Mathlib.Dynamics.BirkhoffSum.Basic
 import Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
 import Mathlib.Dynamics.Ergodic.AddCircle
 import Mathlib.Dynamics.Ergodic.Conservative

Mathlib/Dynamics/BirkhoffSum/Average.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2023 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Dynamics.BirkhoffSum.Basic
+import Mathlib.Algebra.Module.Basic
+
+/-!
+# Birkhoff average
+
+In this file we define `birkhoffAverage f g n x` to be
+$$
+\frac{1}{n}\sum_{k=0}^{n-1}g(f^{[k]}(x)),
+$$
+where `f : α → α` is a self-map on some type `α`,
+`g : α → M` is a function from `α` to a module over a division semiring `R`,
+and `R` is used to formalize division by `n` as `(n : R)⁻¹ • _`.
+
+While we need an auxiliary division semiring `R` to define `birkhoffAverage`,
+the definition does not depend on the choice of `R`,
+see `birkhoffAverage_congr_ring`.
+
+-/
+
+section birkhoffAverage
+
+variable (R : Type _) {α M : Type _} [DivisionSemiring R] [AddCommMonoid M] [Module R M]
+
+/-- The average value of `g` on the first `n` points of the orbit of `x` under `f`,
+i.e. the Birkhoff sum `∑ k in Finset.range n, g (f^[k] x)` divided by `n`.
+
+This average appears in many ergodic theorems
+which say that `(birkhoffAverage R f g · x)`
+converges to the "space average" `⨍ x, g x ∂μ` as `n → ∞`.
+
+We use an auxiliary `[DivisionSemiring R]` to define division by `n`.
+However, the definition does not depend on the choice of `R`,
+see `birkhoffAverage_congr_ring`. -/
+def birkhoffAverage (f : α → α) (g : α → M) (n : ℕ) (x : α) : M := (n : R)⁻¹ • birkhoffSum f g n x
+
+theorem birkhoffAverage_zero (f : α → α) (g : α → M) (x : α) :
+    birkhoffAverage R f g 0 x = 0 := by simp [birkhoffAverage]
+
+@[simp] theorem birkhoffAverage_zero' (f : α → α) (g : α → M) : birkhoffAverage R f g 0 = 0 :=
+  funext <| birkhoffAverage_zero _ _ _
+
+theorem birkhoffAverage_one (f : α → α) (g : α → M) (x : α) :
+    birkhoffAverage R f g 1 x = g x := by simp [birkhoffAverage]
+
+@[simp]
+theorem birkhoffAverage_one' (f : α → α) (g : α → M) : birkhoffAverage R f g 1 = g :=
+  funext <| birkhoffAverage_one R f g
+
+theorem map_birkhoffAverage (S : Type _) {F N : Type _}
+    [DivisionSemiring S] [AddCommMonoid N] [Module S N]
+    [AddMonoidHomClass F M N] (g' : F) (f : α → α) (g : α → M) (n : ℕ) (x : α) :
+    g' (birkhoffAverage R f g n x) = birkhoffAverage S f (g' ∘ g) n x := by
+  simp only [birkhoffAverage, map_inv_nat_cast_smul g' R S, map_birkhoffSum]
+
+theorem birkhoffAverage_congr_ring (S : Type _) [DivisionSemiring S] [Module S M]
+    (f : α → α) (g : α → M) (n : ℕ) (x : α) :
+    birkhoffAverage R f g n x = birkhoffAverage S f g n x :=
+  map_birkhoffAverage R S (AddMonoidHom.id M) f g n x
+
+theorem birkhoffAverage_congr_ring' (S : Type _) [DivisionSemiring S] [Module S M] :
+    birkhoffAverage (α := α) (M := M) R = birkhoffAverage S := by
+  ext; apply birkhoffAverage_congr_ring
+
+theorem Function.IsFixedPt.birkhoffAverage_eq [CharZero R] {f : α → α} {x : α} (h : IsFixedPt f x)
+    (g : α → M) {n : ℕ} (hn : n ≠ 0) : birkhoffAverage R f g n x = g x := by
+  rw [birkhoffAverage, h.birkhoffSum_eq, nsmul_eq_smul_cast R, inv_smul_smul₀]
+  rwa [Nat.cast_ne_zero]
+
+end birkhoffAverage
+
+/-- Birkhoff average is "almost invariant" under `f`:
+the difference between `birkhoffAverage R f g n (f x)` and `birkhoffAverage R f g n x`
+is equal to `(n : R)⁻¹ • (g (f^[n] x) - g x)`. -/
+theorem birkhoffAverage_apply_sub_birkhoffAverage (R : Type _) [DivisionRing R]
+    [AddCommGroup M] [Module R M] (f : α → α) (g : α → M) (n : ℕ) (x : α) :
+    birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x =
+      (n : R)⁻¹ • (g (f^[n] x) - g x) := by
+  simp only [birkhoffAverage, birkhoffSum_apply_sub_birkhoffSum, ← smul_sub]

Mathlib/Dynamics/BirkhoffSum/Basic.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2023 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Algebra.BigOperators.Basic
+import Mathlib.Dynamics.FixedPoints.Basic
+
+/-!
+# Birkhoff sums
+
+In this file we define `birkhoffSum f g n x` to be the sum `∑ k in Finset.range n, g (f^[k] x)`.
+This sum (more precisely, the corresponding average `n⁻¹ • birkhoffSum f g n x`)
+appears in various ergodic theorems
+saying that these averages converge to the "space average" `⨍ x, g x ∂μ` in some sense.
+
+See also `birkhoffAverage` defined in `Dynamics/BirkhoffSum/Average`.
+-/
+
+open Finset Function
+open scoped BigOperators
+
+section AddCommMonoid
+
+variable {α M : Type _} [AddCommMonoid M]
+
+/-- The sum of values of `g` on the first `n` points of the orbit of `x` under `f`. -/
+def birkhoffSum (f : α → α) (g : α → M) (n : ℕ) (x : α) : M := ∑ k in range n, g (f^[k] x)
+
+theorem birkhoffSum_zero (f : α → α) (g : α → M) (x : α) : birkhoffSum f g 0 x = 0 :=
+  sum_range_zero _
+
+@[simp]
+theorem birkhoffSum_zero' (f : α → α) (g : α → M) : birkhoffSum f g 0 = 0 :=
+  funext <| birkhoffSum_zero _ _
+
+theorem birkhoffSum_one (f : α → α) (g : α → M) (x : α) : birkhoffSum f g 1 x = g x :=
+  sum_range_one _
+
+@[simp]
+theorem birkhoffSum_one' (f : α → α) (g : α → M) : birkhoffSum f g 1 = g :=
+  funext <| birkhoffSum_one f g
+
+theorem birkhoffSum_succ (f : α → α) (g : α → M) (n : ℕ) (x : α) :
+    birkhoffSum f g (n + 1) x = birkhoffSum f g n x + g (f^[n] x) :=
+  sum_range_succ _ _
+
+theorem birkhoffSum_succ' (f : α → α) (g : α → M) (n : ℕ) (x : α) :
+    birkhoffSum f g (n + 1) x = g x + birkhoffSum f g n (f x) :=
+  (sum_range_succ' _ _).trans (add_comm _ _)
+
+theorem birkhoffSum_add (f : α → α) (g : α → M) (m n : ℕ) (x : α) :
+    birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x) := by
+  simp_rw [birkhoffSum, sum_range_add, add_comm m, iterate_add_apply]
+
+theorem Function.IsFixedPt.birkhoffSum_eq {f : α → α} {x : α} (h : IsFixedPt f x) (g : α → M)
+    (n : ℕ) : birkhoffSum f g n x = n • g x := by
+  simp [birkhoffSum, (h.iterate _).eq]
+
+theorem map_birkhoffSum {F N : Type _} [AddCommMonoid N] [AddMonoidHomClass F M N]
+    (g' : F) (f : α → α) (g : α → M) (n : ℕ) (x : α) :
+    g' (birkhoffSum f g n x) = birkhoffSum f (g' ∘ g) n x :=
+  map_sum g' _ _
+
+end AddCommMonoid
+
+section AddCommGroup
+
+variable {α G : Type _} [AddCommGroup G]
+
+/-- Birkhoff sum is "almost invariant" under `f`:
+the difference between `birkhoffSum f g n (f x)` and `birkhoffSum f g n x`
+is equal to `g (f^[n] x) - g x`. -/
+theorem birkhoffSum_apply_sub_birkhoffSum (f : α → α) (g : α → G) (n : ℕ) (x : α) :
+    birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x := by
+  rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x),
+    ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x),
+    ← sub_add, ← sub_add, sub_add_comm]
+
+end AddCommGroup