internlm/Lean-Github huggingface dataset:
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : ¬NeBot p
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
simp at h
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : p = ⊥
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : p = ⊥
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
simp [h]
Proof state after:
no goals
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
have f_cont : ContinuousOn f (sphere z₀ r) := F_conv.continuousOn F_cont
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
rw [Metric.tendsto_nhds]
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
intro ε hε
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
have twopir_ne_zero : 2 * Real.pi * r ≠ 0 := by simp [Real.pi_ne_zero, hr.ne.symm]
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
have : (2 * Real.pi * r)⁻¹ * ε > 0 :=
  mul_pos (inv_pos.mpr (mul_pos (mul_pos two_pos Real.pi_pos) hr)) hε.lt
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
filter_upwards [tendstoUniformlyOn_iff.mp F_conv ((2 * Real.pi * r)⁻¹ * ε) this, F_cont] with n h h'
Proof state after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h : ∀ x ∈ sphere z₀ r, dist (f x) (F n x) < (2 * Real.pi * r)⁻¹ * ε
h' : ContinuousOn (F n) (sphere z₀ r)
⊢ dist (∮ (z : ℂ) in C(z₀, r), F n z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h : ∀ x ∈ sphere z₀ r, dist (f x) (F n x) < (2 * Real.pi * r)⁻¹ * ε
h' : ContinuousOn (F n) (sphere z₀ r)
⊢ dist (∮ (z : ℂ) in C(z₀, r), F n z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
simp_rw [dist_comm (f _) _, Complex.dist_eq, ← Complex.norm_eq_abs] at h
Proof state after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ dist (∮ (z : ℂ) in C(z₀, r), F n z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ dist (∮ (z : ℂ) in C(z₀, r), F n z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
rw [Complex.dist_eq, ← circleIntegral.integral_sub (h'.circleIntegrable hr.le) (f_cont.circleIntegrable hr.le),
  ← Complex.norm_eq_abs]
Proof state after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ‖∮ (z : ℂ) in C(z₀, r), F n z - f z‖ < ε
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ‖∮ (z : ℂ) in C(z₀, r), F n z - f z‖ < ε
Tactic:
have : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε := by
  have : z₀ + r ∈ sphere z₀ r := by simp [hr.le, Real.norm_eq_abs]
  exact ⟨z₀ + r, this, h _ this⟩
Proof state after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ‖∮ (z : ℂ) in C(z₀, r), F n z - f z‖ < ε
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ‖∮ (z : ℂ) in C(z₀, r), F n z - f z‖ < ε
Tactic:
convert circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr (h'.sub f_cont) (λ z hz => (h z hz).le) this
Proof state after:
case h.e'_4
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ε = 2 * Real.pi * r * ((2 * Real.pi * r)⁻¹ * ε)
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
case h.e'_4
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ε = 2 * Real.pi * r * ((2 * Real.pi * r)⁻¹ * ε)
Tactic:
field_simp [hr.ne, Real.pi_ne_zero, two_ne_zero]
Proof state after:
case h.e'_4
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ε * (2 * Real.pi * r) = 2 * Real.pi * r * ε
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
case h.e'_4
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ε * (2 * Real.pi * r) = 2 * Real.pi * r * ε
Tactic:
ring
Proof state after:
no goals
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
⊢ 2 * Real.pi * r ≠ 0
Tactic:
simp [Real.pi_ne_zero, hr.ne.symm]
Proof state after:
no goals
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
Tactic:
have : z₀ + r ∈ sphere z₀ r := by simp [hr.le, Real.norm_eq_abs]
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : z₀ + ↑r ∈ sphere z₀ r
⊢ ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : z₀ + ↑r ∈ sphere z₀ r
⊢ ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
Tactic:
exact ⟨z₀ + r, this, h _ this⟩
Proof state after:
no goals
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ z₀ + ↑r ∈ sphere z₀ r
Tactic:
simp [hr.le, Real.norm_eq_abs]
Proof state after:
no goals
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
by_cases h : NeBot p
Proof state after:
case pos
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

case neg
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : ¬NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : ¬NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
case neg => simp at h; simp [h]
Proof state after:
no goals
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : ¬NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
simp at h
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : p = ⊥
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : p = ⊥
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
simp [h]
Proof state after:
no goals
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H1 : IsCompact (sphere z₀ r) := isCompact_sphere z₀ r
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H2 : TendstoUniformlyOn F f p (sphere z₀ r) :=
  (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).1 hf _ hr2 H1
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H3 : DifferentiableOn ℂ f U := hf.differentiableOn hF hU
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H4 : ContinuousOn f (sphere z₀ r) := H3.continuousOn.mono hr2
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H5 : ∀ᶠ n in p, ContinuousOn (F n) (sphere z₀ r) := by
  filter_upwards [hF] with n h using h.continuousOn.mono hr2
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))