Theorem: cauchy2_hasSum_2d
Proof 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
Proof 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)