awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : α → α
g : α → M
n : ℕ
x : α
⊢ birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (g (f^[n] x) - g x)

Tactic:
simp only [birkhoffAverage, birkhoffSum_apply_sub_birkhoffSum, ← smul_sub]

Premises used: birkhoffSum_apply_sub_birkhoffSum, birkhoffAverage, smul_sub
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g : α → M
x : α
⊢ birkhoffSum f g 0 x = 0

Tactic:
sum_range_zero _

Premises used: Finset.sum_range_zero, birkhoffSum
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g : α → M
⊢ birkhoffSum f g 0 = 0

Tactic:
funext <| birkhoffSum_zero _ _

Premises used: birkhoffSum_zero, funext
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g : α → M
x : α
⊢ birkhoffSum f g 1 x = g x

Tactic:
sum_range_one _

Premises used: Finset.sum_range_one, Nat.iterate, birkhoffSum
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g : α → M
⊢ birkhoffSum f g 1 = g

Tactic:
funext <| birkhoffSum_one f g

Premises used: funext, birkhoffSum_one
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g : α → M
n : ℕ
x : α
⊢ birkhoffSum f g (n + 1) x = birkhoffSum f g n x + g (f^[n] x)

Tactic:
sum_range_succ _ _

Premises used: birkhoffSum, Finset.sum_range_succ
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g : α → M
n : ℕ
x : α
⊢ birkhoffSum f g (n + 1) x = g x + birkhoffSum f g n (f x)

Tactic:
(sum_range_succ' _ _).trans (add_comm _ _)

Premises used: add_comm, birkhoffSum, Finset.sum_range_succ', Eq.trans
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g : α → M
m n : ℕ
x : α
simp_rw :
  ∑ k ∈ range (m + n), g (f^[k] x) =
    HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ k ∈ range n, g (f^[k] (f^[m] x)))
simp_rw₁ :
  HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ x_1 ∈ range n, g (f^[m + x_1] x)) =
    HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ k ∈ range n, g (f^[k] (f^[m] x)))
simp_rw₂ :
  HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ x_1 ∈ range n, g (f^[x_1 + m] x)) =
    HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ k ∈ range n, g (f^[k] (f^[m] x)))
⊢ birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)

Tactic:
simp_rw [birkhoffSum, sum_range_add, add_comm m, iterate_add_apply]

Premises used: Function.iterate_add_apply, add_comm, birkhoffSum, Finset.sum_range_add
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g g' : α → M
n : ℕ
x : α
⊢ birkhoffSum f (g + g') n x = birkhoffSum f g n x + birkhoffSum f g' n x

Tactic:
simpa [birkhoffSum] using sum_add_distrib

Premises used: Finset.sum_add_distrib, birkhoffSum
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
⊢ birkhoffSum f g n x = n • g x

Tactic:
simp [birkhoffSum, (h.iterate _).eq]

Premises used: birkhoffSum, Function.IsFixedPt.iterate, Function.IsFixedPt.eq
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
F : Type u_3
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
g' : F
f : α → α
g : α → M
n : ℕ
x : α
⊢ Eq.{u_4 + 1} (α := N) ((g' : (a : M) → N) (birkhoffSum f g n x) : N) (birkhoffSum f ((⇑g' : (a : M) → N) ∘ g) n x : N)

Tactic:
map_sum g' _ _

Premises used: map_sum, birkhoffSum
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
h₁ : ∀ (x : α), birkhoffSum f φ n x = (n • φ) x
⊢ birkhoffSum f φ n = n • φ

Tactic:
funext x
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
x : α
this : ∀ (k : ℕ), φ (f^[k] x) = φ x
⊢ birkhoffSum f φ n x = (n • φ) x

Tactic:
simp [birkhoffSum, this]

Premises used: birkhoffSum
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
x : α
h₁ : ∀ (k : ℕ), φ (f^[k] x) = φ x
⊢ birkhoffSum f φ n x = (n • φ) x

Tactic:
suffices ∀ k, φ (f^[k] x) = φ x by simp [birkhoffSum, this]
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
x : α
k : ℕ
⊢ φ (f^[k] x) = φ x

Tactic:
congrFun (iterate_invariant h k) x

Premises used: congrFun, Function.iterate_invariant
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
x : α
k : ℕ
⊢ φ (f^[k] x) = φ x

Tactic:
exact congrFun (iterate_invariant h k) x

Premises used: congrFun, Function.iterate_invariant
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
G : Type u_2
inst : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f (-g) n x = -birkhoffSum f g n x

Tactic:
simp [birkhoffSum]

Premises used: birkhoffSum
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
G : Type u_2
inst : AddCommGroup G
f : α → α
g g' : α → G
n : ℕ
x : α
⊢ birkhoffSum f (g - g') n x = birkhoffSum f g n x - birkhoffSum f g' n x

Tactic:
simp [birkhoffSum]

Premises used: birkhoffSum
-- Module: Mathlib.Dynamics.BirkhoffSum.Basic
Goal:
α : Type u_1
G : Type u_2
inst : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
rw : birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) = g (f^[n] x) - g x
rw₁ :
  birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
rw₂ :
  birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
rw₃ :
  birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
    g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x)
rw₄ rw₅ :
  g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x) =
    g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x)
⊢ birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x

Tactic:
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]

Premises used: sub_add, Iff.mpr, birkhoffSum_succ, sub_eq_iff_eq_add, sub_add_comm, birkhoffSum_succ'
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
R : Type u_3
inst : DivisionSemiring R
inst_1 : CharZero R
inst_2 : AddCommMonoid E
inst_3 : TopologicalSpace E
inst_4 : Module R E
f : α → α
x : α
h : IsFixedPt f x
g : α → E
⊢ Tendsto (fun (x_1 : ℕ) ↦ birkhoffAverage R f g x_1 x) atTop (𝓝 (g x))

Tactic:
tendsto_const_nhds.congr' <| (eventually_ne_atTop 0).mono fun _n hn ↦
    (h.birkhoffAverage_eq R g (Nat.cast_ne_zero.mpr hn)).symm

Premises used: Iff.mpr, tendsto_const_nhds, Filter.eventually_ne_atTop, Function.IsFixedPt.birkhoffAverage_eq, Filter.Eventually.mono, Filter.Tendsto.congr', OfNat.ofNat, Eq.symm, Nat.cast_ne_zero
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
f : α → α
g : α → E
n : ℕ
x : α
⊢ dist (birkhoffSum f g n (f x)) (birkhoffSum f g n x) = dist (g (f^[n] x)) (g x)

Tactic:
simp only [dist_eq_norm, birkhoffSum_apply_sub_birkhoffSum]

Premises used: dist_eq_norm, birkhoffSum_apply_sub_birkhoffSum
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
f : α → α
g : α → E
n : ℕ
x y : α
⊢ dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))

Tactic:
dist_sum_sum_le _ _ _

Premises used: birkhoffSum, dist_sum_sum_le
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
n : ℕ
x y : α
⊢ dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) =
    dist (birkhoffSum f g n x) (birkhoffSum f g n y) / (↑n : ℝ)

Tactic:
simp [birkhoffAverage, dist_smul₀, div_eq_inv_mul]

Premises used: birkhoffAverage, dist_smul₀, div_eq_inv_mul
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
n : ℕ
x y : α
hab : dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))
⊢ dist (birkhoffSum f g n x) (birkhoffSum f g n y) / (↑n : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
n : ℕ
x y : α
⊢ dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))

Tactic:
apply dist_birkhoffSum_birkhoffSum_le

Premises used: dist_birkhoffSum_birkhoffSum_le
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
n : ℕ
x : α
⊢ dist (birkhoffAverage 𝕜 f g n (f x)) (birkhoffAverage 𝕜 f g n x) = dist (g (f^[n] x)) (g x) / (↑n : ℝ)

Tactic:
simp [dist_birkhoffAverage_birkhoffAverage, dist_birkhoffSum_apply_birkhoffSum]

Premises used: dist_birkhoffAverage_birkhoffAverage, dist_birkhoffSum_apply_birkhoffSum
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
rcases :
  ∀ (C : ℝ) (hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)

Tactic:
rcases Metric.isBounded_range_iff.1 h with ⟨C, hC⟩

Premises used: Iff.mp, Metric.isBounded_range_iff
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)

Tactic:
have : Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) :=
    tendsto_const_nhds.div_atTop tendsto_natCast_atTop_atTop
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)

Tactic:
squeeze_zero_norm (fun n ↦ ?_) this

Premises used: squeeze_zero_norm
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)
refine : ∀ (n : ℕ), ‖birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x‖ ≤ C / (↑n : ℝ)
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)

Tactic:
refine squeeze_zero_norm (fun n ↦ ?_) this

Premises used: squeeze_zero_norm
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
rw : dist (g (f^[n] x)) (g x) / (↑n : ℝ) ≤ C / (↑n : ℝ)
⊢ ‖birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x‖ ≤ C / (↑n : ℝ)

Tactic:
rw [← dist_eq_norm, dist_birkhoffAverage_apply_birkhoffAverage]

Premises used: dist_eq_norm, dist_birkhoffAverage_apply_birkhoffAverage
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
hab : dist (g (f^[n] x)) (g x) ≤ C
⊢ dist (g (f^[n] x)) (g x) / (↑n : ℝ) ≤ C / (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
⊢ dist (g (f^[n] x)) (g x) ≤ C

Tactic:
hC n 0

Premises used: Nat.iterate, OfNat.ofNat
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
⊢ dist (g (f^[n] x)) (g x) ≤ C

Tactic:
exact hC n 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
g : α → E
h : Bornology.IsBounded (range g)
f : α → α
x : α
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)

Tactic:
tendsto_birkhoffAverage_apply_sub_birkhoffAverage _ <| h.subset <| range_comp_subset_range _ _

Premises used: Set.range_comp_subset_range, tendsto_birkhoffAverage_apply_sub_birkhoffAverage, Bornology.IsBounded.subset
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
⊢ UniformEquicontinuous (birkhoffAverage 𝕜 f g)

Tactic:
Metric.uniformity_basis_dist_le.uniformEquicontinuous_iff_right.2 fun ε hε ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.uniformEquicontinuous_iff_right, Metric.uniformity_basis_dist_le
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
refine :
  ∀ (ε : ℝ) (hε : 0 < ε),
    ∀ᶠ (xy : X × X) in 𝓤 X,
      ∀ (i : ℕ),
        Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
          (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2)
⊢ UniformEquicontinuous (birkhoffAverage 𝕜 f g)

Tactic:
refine Metric.uniformity_basis_dist_le.uniformEquicontinuous_iff_right.2 fun ε hε ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.uniformEquicontinuous_iff_right, Metric.uniformity_basis_dist_le
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
rcases :
  ∀ (δ : ℝ≥0∞) (hδ₀ : 0 < δ)
    (hδε :
      ∀ (x y : X),
        Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
          Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)),
    ∀ᶠ (xy : X × X) in 𝓤 X,
      ∀ (i : ℕ),
        Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
          (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2)
⊢ ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ),
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
        (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2)

Tactic:
rcases (uniformity_basis_edist_le.uniformContinuous_iff Metric.uniformity_basis_dist_le).1 hg ε hε
    with ⟨δ, hδ₀, hδε⟩

Premises used: uniformity_basis_edist_le, Metric.uniformity_basis_dist_le, Filter.HasBasis.uniformContinuous_iff, Iff.mp
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
⊢ ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ),
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
        (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2)

Tactic:
mem_uniformity_edist.2 ⟨δ, hδ₀, fun {x y} h n ↦ ?_⟩

Premises used: Iff.mpr, Filter.Eventually, And.intro, Exists.intro, mem_uniformity_edist
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
refine :
  ∀ {x y : X} (h : edist x y < δ) (n : ℕ),
    Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
      (birkhoffAverage 𝕜 f g n (x, y).1, birkhoffAverage 𝕜 f g n (x, y).2)
⊢ ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ),
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
        (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2)

Tactic:
refine mem_uniformity_edist.2 ⟨δ, hδ₀, fun {x y} h n ↦ ?_⟩
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
⊢ dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) ≤
    HDiv.hDiv (α := ℝ) (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) (↑n : ℝ)

Tactic:
dist_birkhoffAverage_birkhoffAverage_le ..

Premises used: dist_birkhoffAverage_birkhoffAverage_le
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
hab : ∀ i ∈ Finset.range n, dist (g (f^[i] x)) (g (f^[i] y)) ≤ ε
⊢ HDiv.hDiv (α := ℝ) (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) (↑n : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ _k ∈ Finset.range n, ε) (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n i : ℕ
h_1 : i ∈ Finset.range n
⊢ dist (g (f^[i] x)) (g (f^[i] y)) ≤ ε

Tactic:
hδε _ _ ?_

Premises used: Set.Mem
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n i : ℕ
h_1 : i ∈ Finset.range n
hab : Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (f^[i] x, f^[i] y)
⊢ dist (g (f^[i] x)) (g (f^[i] y)) ≤ ε

Tactic:
refine hδε _ _ ?_
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n i : ℕ
h_1 : i ∈ Finset.range n
⊢ Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (f^[i] x, f^[i] y)

Tactic:
simpa using (hf.iterate _).edist_le_mul_of_le h.le

Premises used: LT.lt.le, LipschitzWith.edist_le_mul_of_le, LipschitzWith.iterate
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (∑ _k ∈ Finset.range n, ε) (↑n : ℝ) = (↑n : ℝ) * ε / (↑n : ℝ)

Tactic:
simp