Theorem: cauchy2_hasSum_2d (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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
⊢ HasSum (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) (f (c0 + w0, c1 + w1))
Tactic:
generalize ha : f (c0 + w0, c1 + w1) = a
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f (c0 + w0, c1 + w1) = a
⊢ HasSum (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) a

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f (c0 + w0, c1 + w1) = a
⊢ HasSum (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) a
Tactic:
generalize hf : (fun n : ℕ × ℕ ↦ w0 ^ n.snd • w1 ^ n.fst • h.series2Coeff n.snd n.fst) = f
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
⊢ HasSum f a

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
⊢ HasSum f a
Tactic:
generalize hg : (fun n1 : ℕ ↦ w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
⊢ HasSum f a

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
⊢ HasSum f a
Tactic:
generalize ha' : ∑' n, f n = a'
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
⊢ HasSum f a

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
⊢ HasSum f a
Tactic:
have gs : HasSum g a := by rw [← hg, ← ha]; exact cauchy2_hasSum_n1n0 h w0m w1m
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
⊢ HasSum f a

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
⊢ HasSum f a
Tactic:
have fs : ∀ n1 : ℕ, HasSum (fun n0 ↦ f ⟨n1, n0⟩) (g n1) := by
  intro n1; rw [← hf, ← hg]; simp only
  simp_rw [smul_comm (w0 ^ _) _]; apply HasSum.const_smul; exact cauchy2_hasSum_n0 h w0m n1
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
⊢ HasSum f a

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
sf : Summable f
⊢ HasSum f a
Tactic:
have fs' : HasSum f a' := by rw [← ha']; exact sf.hasSum
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
sf : Summable f
fs' : HasSum f a'
⊢ HasSum f a

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
sf : Summable f
fs' : HasSum f a'
⊢ HasSum f a
Tactic:
have gs' := HasSum.prod_fiberwise fs' fs
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
sf : Summable f
fs' : HasSum f a'
gs' : HasSum (fun b => g b) a'
⊢ HasSum f a

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
sf : Summable f
fs' : HasSum f a'
gs' : HasSum (fun b => g b) a'
⊢ HasSum f a
Tactic:
rwa [HasSum.unique gs gs']
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
⊢ HasSum g a
Tactic:
rw [← hg, ← ha]
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f✝ (c0 + w0, c1 + 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f✝ (c0 + w0, c1 + w1))
Tactic:
exact cauchy2_hasSum_n1n0 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
⊢ ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
Tactic:
intro n1
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
n1 : ℕ
⊢ HasSum (fun n0 => f (n1, n0)) (g n1)

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
n1 : ℕ
⊢ HasSum (fun n0 => f (n1, n0)) (g n1)
Tactic:
rw [← hf, ← hg]
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
n1 : ℕ
⊢ HasSum (fun n0 => (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) (n1, n0))
    ((fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) n1)

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
n1 : ℕ
⊢ HasSum (fun n0 => (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) (n1, n0))
    ((fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) n1)
Tactic:
simp only
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
n1 : ℕ
⊢ HasSum (fun n0 => w0 ^ n0 • w1 ^ n1 • h.series2Coeff n0 n1) (w1 ^ n1 • h.series2CoeffN0Sum n1 w0)

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
n1 : ℕ
⊢ HasSum (fun n0 => w0 ^ n0 • w1 ^ n1 • h.series2Coeff n0 n1) (w1 ^ n1 • h.series2CoeffN0Sum n1 w0)
Tactic:
simp_rw [smul_comm (w0 ^ _) _]
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
n1 : ℕ
⊢ HasSum (fun n0 => w1 ^ n1 • w0 ^ n0 • h.series2Coeff n0 n1) (w1 ^ n1 • h.series2CoeffN0Sum n1 w0)

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
n1 : ℕ
⊢ HasSum (fun n0 => w1 ^ n1 • w0 ^ n0 • h.series2Coeff n0 n1) (w1 ^ n1 • h.series2CoeffN0Sum n1 w0)
Tactic:
apply HasSum.const_smul
State after:
case hf
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
n1 : ℕ
⊢ HasSum (fun i => w0 ^ i • h.series2Coeff i n1) (h.series2CoeffN0Sum n1 w0)

State before:
case hf
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
n1 : ℕ
⊢ HasSum (fun i => w0 ^ i • h.series2Coeff i n1) (h.series2CoeffN0Sum n1 w0)
Tactic:
exact cauchy2_hasSum_n0 h w0m n1
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
⊢ ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
Tactic:
intro n
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
Tactic:
rw [← hf]
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ ‖(fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) n‖ ≤
    b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ ‖(fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) n‖ ≤
    b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ ‖w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1‖ ≤
    b * (Complex.abs w0 ^ n.2 / r ^ n.2) * (Complex.abs w1 ^ n.1 / r ^ n.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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ ‖w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1‖ ≤
    b * (Complex.abs w0 ^ n.2 / r ^ n.2) * (Complex.abs w1 ^ n.1 / r ^ n.1)
Tactic:
rw [norm_smul, norm_smul, mul_assoc]
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ ‖w0 ^ n.2‖ * (‖w1 ^ n.1‖ * ‖h.series2Coeff n.2 n.1‖) ≤
    b * (Complex.abs w0 ^ n.2 / r ^ n.2 * (Complex.abs w1 ^ n.1 / r ^ n.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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ ‖w0 ^ n.2‖ * (‖w1 ^ n.1‖ * ‖h.series2Coeff n.2 n.1‖) ≤
    b * (Complex.abs w0 ^ n.2 / r ^ n.2 * (Complex.abs w1 ^ n.1 / r ^ n.1))
Tactic:
rw [Complex.norm_eq_abs, Complex.norm_eq_abs, ← mul_assoc]
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs (w0 ^ n.2) * Complex.abs (w1 ^ n.1) * ‖h.series2Coeff n.2 n.1‖ ≤
    b * (Complex.abs w0 ^ n.2 / r ^ n.2 * (Complex.abs w1 ^ n.1 / r ^ n.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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs (w0 ^ n.2) * Complex.abs (w1 ^ n.1) * ‖h.series2Coeff n.2 n.1‖ ≤
    b * (Complex.abs w0 ^ n.2 / r ^ n.2 * (Complex.abs w1 ^ n.1 / r ^ n.1))
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * ‖h.series2Coeff n.2 n.1‖ ≤
    b * (Complex.abs w0 ^ n.2 / r ^ n.2 * (Complex.abs w1 ^ n.1 / r ^ n.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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * ‖h.series2Coeff n.2 n.1‖ ≤
    b * (Complex.abs w0 ^ n.2 / r ^ n.2 * (Complex.abs w1 ^ n.1 / r ^ n.1))
Tactic:
trans abs w0 ^ n.snd * abs w1 ^ n.fst * (b * r⁻¹ ^ (n.snd + n.fst))
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * ‖h.series2Coeff n.2 n.1‖ ≤
    Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * (b * r⁻¹ ^ (n.2 + n.1))

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * (b * r⁻¹ ^ (n.2 + n.1)) ≤
    b * (Complex.abs w0 ^ n.2 / r ^ n.2 * (Complex.abs w1 ^ n.1 / r ^ n.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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * ‖h.series2Coeff n.2 n.1‖ ≤
    Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * (b * r⁻¹ ^ (n.2 + n.1))
Tactic:
bound [series2Coeff_bound h n.snd n.fst]
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * (b * r⁻¹ ^ (n.2 + n.1)) ≤
    b * (Complex.abs w0 ^ n.2 / r ^ n.2 * (Complex.abs w1 ^ n.1 / r ^ n.1))
Tactic:
rw [pow_add, div_eq_mul_inv, div_eq_mul_inv, inv_pow, inv_pow]
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * (b * ((r ^ n.2)⁻¹ * (r ^ n.1)⁻¹)) ≤
    b * (Complex.abs w0 ^ n.2 * (r ^ n.2)⁻¹ * (Complex.abs w1 ^ n.1 * (r ^ n.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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * (b * ((r ^ n.2)⁻¹ * (r ^ n.1)⁻¹)) ≤
    b * (Complex.abs w0 ^ n.2 * (r ^ n.2)⁻¹ * (Complex.abs w1 ^ n.1 * (r ^ n.1)⁻¹))
Tactic:
ring_nf
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * b * r⁻¹ ^ n.2 * r⁻¹ ^ n.1 ≤
    Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * b * r⁻¹ ^ n.2 * r⁻¹ ^ n.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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
n : ℕ × ℕ
⊢ Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * b * r⁻¹ ^ n.2 * r⁻¹ ^ n.1 ≤
    Complex.abs w0 ^ n.2 * Complex.abs w1 ^ n.1 * b * r⁻¹ ^ n.2 * r⁻¹ ^ n.1
Tactic:
rfl
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
⊢ Summable f
Tactic:
simp only [Metric.mem_ball, dist_zero_right, Complex.norm_eq_abs] at w0m w1m
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable f

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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable f
Tactic:
refine .of_norm_bounded _ ?_ fb
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable fun i => b * (Complex.abs w0 / r) ^ i.2 * (Complex.abs w1 / r) ^ i.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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable fun i => b * (Complex.abs w0 / r) ^ i.2 * (Complex.abs w1 / r) ^ i.1
Tactic:
simp_rw [mul_assoc]
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable fun i => b * ((Complex.abs w0 / r) ^ i.2 * (Complex.abs w1 / r) ^ i.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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable fun i => b * ((Complex.abs w0 / r) ^ i.2 * (Complex.abs w1 / r) ^ i.1)
Tactic:
apply Summable.mul_left
State after:
case hf
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable fun i => (Complex.abs w0 / r) ^ i.2 * (Complex.abs w1 / r) ^ i.1

State before:
case hf
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable fun i => (Complex.abs w0 / r) ^ i.2 * (Complex.abs w1 / r) ^ i.1
Tactic:
simp_rw [mul_comm ((abs w0 / r) ^ _) _]
State after:
case hf
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable fun i => (Complex.abs w1 / r) ^ i.1 * (Complex.abs w0 / r) ^ i.2

State before:
case hf
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable fun i => (Complex.abs w1 / r) ^ i.1 * (Complex.abs w0 / r) ^ i.2
Tactic:
apply Summable.mul_of_nonneg
State after:
case hf.hf
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable (HPow.hPow (Complex.abs w1 / r))

case hf.hg
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable (HPow.hPow (Complex.abs w0 / r))

case hf.hf'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ 0 ≤ HPow.hPow (Complex.abs w1 / r)

case hf.hg'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ 0 ≤ HPow.hPow (Complex.abs w0 / r)

State before:
case hf.hf
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable (HPow.hPow (Complex.abs w1 / r))
Tactic:
exact summable_geometric_of_lt_one (by bound) ((div_lt_one h.rp).mpr 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
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ 0 ≤ Complex.abs w1 / r
Tactic:
bound
State after:
no goals

State before:
case hf.hg
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ Summable (HPow.hPow (Complex.abs w0 / r))
Tactic:
exact summable_geometric_of_lt_one (by bound) ((div_lt_one h.rp).mpr w0m)
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
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ 0 ≤ Complex.abs w0 / r
Tactic:
bound
State after:
no goals

State before:
case hf.hf'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ 0 ≤ HPow.hPow (Complex.abs w1 / r)
Tactic:
intro n
State after:
case hf.hf'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
n : ℕ
⊢ 0 n ≤ (Complex.abs w1 / r) ^ n

State before:
case hf.hf'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
n : ℕ
⊢ 0 n ≤ (Complex.abs w1 / r) ^ n
Tactic:
simp only [Pi.zero_apply, div_pow]
State after:
case hf.hf'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
n : ℕ
⊢ 0 ≤ Complex.abs w1 ^ n / r ^ n

State before:
case hf.hf'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
n : ℕ
⊢ 0 ≤ Complex.abs w1 ^ n / r ^ n
Tactic:
bound
State after:
no goals

State before:
case hf.hg'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
⊢ 0 ≤ HPow.hPow (Complex.abs w0 / r)
Tactic:
intro n
State after:
case hf.hg'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
n : ℕ
⊢ 0 n ≤ (Complex.abs w0 / r) ^ n

State before:
case hf.hg'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
n : ℕ
⊢ 0 n ≤ (Complex.abs w0 / r) ^ n
Tactic:
simp only [Pi.zero_apply, div_pow]
State after:
case hf.hg'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
n : ℕ
⊢ 0 ≤ Complex.abs w0 ^ n / r ^ n

State before:
case hf.hg'
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 : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
w0m : Complex.abs w0 < r
w1m : Complex.abs w1 < r
n : ℕ
⊢ 0 ≤ Complex.abs w0 ^ n / r ^ n
Tactic:
bound
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
sf : Summable f
⊢ HasSum f a'
Tactic:
rw [← ha']
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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
sf : Summable f
⊢ HasSum f (∑' (n : ℕ × ℕ), f n)

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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
ha : f✝ (c0 + w0, c1 + w1) = a
f : ℕ × ℕ → E
hf : (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) = f
g : ℕ → E
hg : (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = g
a' : E
ha' : ∑' (n : ℕ × ℕ), f n = a'
gs : HasSum g a
fs : ∀ (n1 : ℕ), HasSum (fun n0 => f (n1, n0)) (g n1)
fb : ∀ (n : ℕ × ℕ), ‖f n‖ ≤ b * (Complex.abs w0 / r) ^ n.2 * (Complex.abs w1 / r) ^ n.1
sf : Summable f
⊢ HasSum f (∑' (n : ℕ × ℕ), f n)
Tactic:
exact sf.hasSum
State after:
no goals