internlm/Lean-Github huggingface dataset:
Theorem: cauchy2_hasSum_2d
Proof 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 ^ _) _]
Proof 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)
Theorem: cauchy2_hasSum_2d
Proof 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
Proof 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)
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
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
Proof state after:
no goals
Theorem: cauchy2_hasSum_2d
Proof 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
Proof 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
Theorem: cauchy2_hasSum_2d
Proof 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]
Proof 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
Theorem: cauchy2_hasSum_2d
Proof 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
Proof 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)
Theorem: cauchy2_hasSum_2d
Proof 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]
Proof 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))
Theorem: cauchy2_hasSum_2d
Proof 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]
Proof 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))
Theorem: cauchy2_hasSum_2d
Proof 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
Proof 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))
Theorem: cauchy2_hasSum_2d
Proof 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))
Proof 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))
Theorem: cauchy2_hasSum_2d
Proof 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]
Proof state after:
no goals
Theorem: cauchy2_hasSum_2d
Proof 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]
Proof 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)⁻¹))
Theorem: cauchy2_hasSum_2d
Proof 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
Proof 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
Theorem: cauchy2_hasSum_2d
Proof 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
Proof state after:
no goals
Theorem: cauchy2_hasSum_2d
Proof 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
Proof 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
Theorem: cauchy2_hasSum_2d
Proof 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
Proof 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
Theorem: cauchy2_hasSum_2d
Proof 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]
Proof 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)
Theorem: cauchy2_hasSum_2d
Proof 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
Proof 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