[GOAL]
R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
g : α → M
x : α
⊢ birkhoffAverage R f g 0 x = 0
[PROOFSTEP]
simp [birkhoffAverage]
[GOAL]
R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
g : α → M
x : α
⊢ birkhoffAverage R f g 1 x = g x
[PROOFSTEP]
simp [birkhoffAverage]
[GOAL]
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁶ : DivisionSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
F : Type u_5
N : Type u_6
inst✝³ : DivisionSemiring S
inst✝² : AddCommMonoid N
inst✝¹ : Module S N
inst✝ : 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
[PROOFSTEP]
simp only [birkhoffAverage, map_inv_nat_cast_smul g' R S, map_birkhoffSum]
[GOAL]
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : DivisionSemiring S
inst✝ : Module S M
⊢ birkhoffAverage R = birkhoffAverage S
[PROOFSTEP]
ext
[GOAL]
case h.h.h.h
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : DivisionSemiring S
inst✝ : Module S M
x✝³ : α → α
x✝² : α → M
x✝¹ : ℕ
x✝ : α
⊢ birkhoffAverage R x✝³ x✝² x✝¹ x✝ = birkhoffAverage S x✝³ x✝² x✝¹ x✝
[PROOFSTEP]
apply birkhoffAverage_congr_ring
[GOAL]
R : Type u_1
α : Type u_2
M : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CharZero R
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : n ≠ 0
⊢ birkhoffAverage R f g n x = g x
[PROOFSTEP]
rw [birkhoffAverage, h.birkhoffSum_eq, nsmul_eq_smul_cast R, inv_smul_smul₀]
[GOAL]
case hc
R : Type u_1
α : Type u_2
M : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CharZero R
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
[PROOFSTEP]
rwa [Nat.cast_ne_zero]
[GOAL]
M : Type u_2
α : Type u_3
R : Type u_1
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : α → α
g : α → M
n : ℕ
x : α
⊢ birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x = (↑n)⁻¹ • (g (f^[n] x) - g x)
[PROOFSTEP]
simp only [birkhoffAverage, birkhoffSum_apply_sub_birkhoffSum, ← smul_sub]
