Theorem: osgood_h (Ray/Hartogs/Osgood.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
⊢ 0 < ENNReal.ofReal r
Tactic:
simp
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
⊢ 0 < r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
⊢ 0 < r
Tactic:
exact h.rp
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
⊢ ∀ {y : ℂ × ℂ}, y ∈ EMetric.ball 0 (ENNReal.ofReal r) → HasSum (fun n => (series2 h n) fun x => y) (f ((c0, c1) + y))
Tactic:
simp only [Metric.emetric_ball, Metric.mem_ball, dist_zero_right, Prod.forall]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
⊢ ∀ (a b_1 : ℂ), ‖(a, b_1)‖ < r → HasSum (fun n => (series2 h n) fun x => (a, b_1)) (f ((c0, c1) + (a, b_1)))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
⊢ ∀ (a b_1 : ℂ), ‖(a, b_1)‖ < r → HasSum (fun n => (series2 h n) fun x => (a, b_1)) (f ((c0, c1) + (a, b_1)))
Tactic:
intro w0 w1 wr
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : ‖(w0, w1)‖ < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : ‖(w0, w1)‖ < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Tactic:
rw [Prod.norm_def] at wr
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : max ‖(w0, w1).1‖ ‖(w0, w1).2‖ < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : max ‖(w0, w1).1‖ ‖(w0, w1).2‖ < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Tactic:
simp only [Complex.norm_eq_abs, ge_iff_le, max_lt_iff] at wr
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Tactic:
have w0m : w0 ∈ ball (0 : ℂ) r := by simp; exact wr.left
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Tactic:
have w1m : w1 ∈ ball (0 : ℂ) r := by simp; exact wr.right
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Tactic:
exact cauchy2_hasSum h w0m w1m
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
⊢ w0 ∈ ball 0 r
Tactic:
simp
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
⊢ Complex.abs w0 < r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
⊢ Complex.abs w0 < r
Tactic:
exact wr.left
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
⊢ w1 ∈ ball 0 r
Tactic:
simp
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
⊢ Complex.abs w1 < r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0✝ w1✝ : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
⊢ Complex.abs w1 < r
Tactic:
exact wr.right
State after:
no goals