-- Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean
theorem uniformEquicontinuous_birkhoffAverage (hf : LipschitzWith 1 f) (hg : UniformContinuous g) :
    UniformEquicontinuous (birkhoffAverage 𝕜 f g)

Proof state:
case intro.intro
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
⊢ ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ), (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2) ∈ {p | dist p.1 p.2 ≤ ε}

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

Result:
case intro.intro
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n : ℕ
⊢ (birkhoffAverage 𝕜 f g n (x, y).1, birkhoffAverage 𝕜 f g n (x, y).2) ∈ {p | dist p.1 p.2 ≤ ε}

Proof state:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n : ℕ
⊢ (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / ↑n ≤ (∑ _k ∈ Finset.range n, ε) / ↑n

Tactic:
gcongr

Result:
case hab.h
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ dist (g (f^[i✝] x)) (g (f^[i✝] y)) ≤ ε

Proof state:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n : ℕ
⊢ ↑n * ε / ↑n ≤ ε

Tactic:
rcases eq_or_ne n 0 with hn | hn <;> field_simp [hn, hε.le, mul_div_cancel_left₀]

Result:
no goals

Proof state:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n : ℕ
⊢ (∑ _k ∈ Finset.range n, ε) / ↑n = ↑n * ε / ↑n

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n : ℕ
⊢ (birkhoffAverage 𝕜 f g n (x, y).1, birkhoffAverage 𝕜 f g n (x, y).2) ∈ {p | dist p.1 p.2 ≤ ε}

Tactic:
calc
  dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y)
    ≤ (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / n :=
    dist_birkhoffAverage_birkhoffAverage_le ..
  _ ≤ (∑ _k ∈ Finset.range n, ε) / n := by
    gcongr
    refine hδε _ _ ?_
    simpa using (hf.iterate _).edist_le_mul_of_le h.le
  _ = n * ε / n := by simp
  _ ≤ ε := by
    rcases eq_or_ne n 0 with hn | hn <;> field_simp [hn, hε.le, mul_div_cancel_left₀]

Result:
no goals

Proof state:
case hab.h
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ (f^[i✝] x, f^[i✝] y) ∈ {p | edist p.1 p.2 ≤ δ}

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

Result:
no goals

Proof state:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ), (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2) ∈ {p | dist p.1 p.2 ≤ ε}

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

Result:
case intro.intro
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
⊢ ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ), (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2) ∈ {p | dist p.1 p.2 ≤ ε}

Proof state:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
⊢ UniformEquicontinuous (birkhoffAverage 𝕜 f g)

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

Result:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ), (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2) ∈ {p | dist p.1 p.2 ≤ ε}

Proof state:
case hab.h
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ dist (g (f^[i✝] x)) (g (f^[i✝] y)) ≤ ε

Tactic:
refine hδε _ _ ?_

Result:
case hab.h
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ (f^[i✝] x, f^[i✝] y) ∈ {p | edist p.1 p.2 ≤ δ}