internlm/Lean-Github huggingface dataset:
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 w0 / r) ^ i.2 * (Complex.abs w1 / r) ^ i.1
Tactic:
simp_rw [mul_comm ((abs w0 / r) ^ _) _]
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 w1 / r) ^ i.1 * (Complex.abs w0 / r) ^ i.2
Theorem: cauchy2_hasSum_2d
Proof 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)
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
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
Proof state after:
no goals
Theorem: cauchy2_hasSum_2d
Proof 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)
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
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
Proof state after:
no goals
Theorem: cauchy2_hasSum_2d
Proof 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
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
n : ℕ
⊢ 0 n ≤ (Complex.abs w1 / r) ^ n
Theorem: cauchy2_hasSum_2d
Proof 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]
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
n : ℕ
⊢ 0 ≤ Complex.abs w1 ^ n / r ^ n
Theorem: cauchy2_hasSum_2d
Proof 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
Proof state after:
no goals
Theorem: cauchy2_hasSum_2d
Proof 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
Proof 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
Theorem: cauchy2_hasSum_2d
Proof 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]
Proof 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
Theorem: cauchy2_hasSum_2d
Proof 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
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
sf : Summable f
⊢ HasSum f a'
Tactic:
rw [← ha']
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)
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)
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
sf : Summable f
⊢ HasSum f (∑' (n : ℕ × ℕ), f n)
Tactic:
exact sf.hasSum
Proof state after:
no goals
Theorem: HasSum.antidiagonal_of_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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum f a
⊢ HasSum (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) a
Tactic:
generalize hg : (fun n ↦ (Finset.range (n + 1)).sum fun n1 ↦ f (n1, n - n1)) = g
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum f a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
⊢ HasSum g a
Theorem: HasSum.antidiagonal_of_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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum f a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
⊢ HasSum g a
Tactic:
rw [←Finset.sigmaAntidiagonalEquivProd.hasSum_iff] at h
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
⊢ HasSum g a
Theorem: HasSum.antidiagonal_of_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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
⊢ HasSum g a
Tactic:
have fg : ∀ n, HasSum (fun d : Finset.antidiagonal n ↦
    (f ∘ Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n) := by
  intro n; simp only [Function.comp_apply, Finset.sigmaAntidiagonalEquivProd_apply]
  have fs := hasSum_fintype fun d : ↥(Finset.antidiagonal n) ↦ f ↑d
  have e : (Finset.univ.sum fun d : ↥(Finset.antidiagonal n) ↦ f ↑d) = g n := by
    rw [Finset.sum_coe_sort, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, ← hg]
  rwa [← e]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
fg : ∀ (n : ℕ), HasSum (fun d => (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n)
⊢ HasSum g a
Theorem: HasSum.antidiagonal_of_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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
fg : ∀ (n : ℕ), HasSum (fun d => (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n)
⊢ HasSum g a
Tactic:
exact HasSum.sigma h fg
Proof state after:
no goals
Theorem: HasSum.antidiagonal_of_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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
⊢ ∀ (n : ℕ), HasSum (fun d => (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n)
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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
⊢ HasSum (fun d => (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n)
Theorem: HasSum.antidiagonal_of_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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
⊢ HasSum (fun d => (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n)
Tactic:
simp only [Function.comp_apply, Finset.sigmaAntidiagonalEquivProd_apply]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
⊢ HasSum (fun d => f ↑d) (g n)
Theorem: HasSum.antidiagonal_of_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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
⊢ HasSum (fun d => f ↑d) (g n)
Tactic:
have fs := hasSum_fintype fun d : ↥(Finset.antidiagonal n) ↦ f ↑d
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
fs : HasSum (fun d => f ↑d) (Finset.univ.sum fun b => f ↑b)
⊢ HasSum (fun d => f ↑d) (g n)
Theorem: HasSum.antidiagonal_of_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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
fs : HasSum (fun d => f ↑d) (Finset.univ.sum fun b => f ↑b)
⊢ HasSum (fun d => f ↑d) (g n)
Tactic:
have e : (Finset.univ.sum fun d : ↥(Finset.antidiagonal n) ↦ f ↑d) = g n := by
  rw [Finset.sum_coe_sort, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, ← hg]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
fs : HasSum (fun d => f ↑d) (Finset.univ.sum fun b => f ↑b)
e : (Finset.univ.sum fun d => f ↑d) = g n
⊢ HasSum (fun d => f ↑d) (g n)
Theorem: HasSum.antidiagonal_of_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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
fs : HasSum (fun d => f ↑d) (Finset.univ.sum fun b => f ↑b)
e : (Finset.univ.sum fun d => f ↑d) = g n
⊢ HasSum (fun d => f ↑d) (g n)
Tactic:
rwa [← e]
Proof state after:
no goals
Theorem: HasSum.antidiagonal_of_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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
fs : HasSum (fun d => f ↑d) (Finset.univ.sum fun b => f ↑b)
⊢ (Finset.univ.sum fun d => f ↑d) = g n
Tactic:
rw [Finset.sum_coe_sort, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, ← hg]
Proof state after:
no goals
Theorem: cauchy2_hasSum
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
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f (c0 + w0, c1 + w1))
Tactic:
have sum := (cauchy2_hasSum_2d h w0m w1m).antidiagonal_of_2d
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
sum :
  HasSum
    (fun n =>
      (Finset.range (n + 1)).sum fun n1 =>
        w0 ^ (n1, n - n1).2 • w1 ^ (n1, n - n1).1 • h.series2Coeff (n1, n - n1).2 (n1, n - n1).1)
    (f (c0 + w0, c1 + w1))
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f (c0 + w0, c1 + w1))
Theorem: cauchy2_hasSum
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
sum :
  HasSum
    (fun n =>
      (Finset.range (n + 1)).sum fun n1 =>
        w0 ^ (n1, n - n1).2 • w1 ^ (n1, n - n1).1 • h.series2Coeff (n1, n - n1).2 (n1, n - n1).1)
    (f (c0 + w0, c1 + w1))
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f (c0 + w0, c1 + w1))
Tactic:
simp only [ge_iff_le] at sum
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
sum :
  HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x)
    (f (c0 + w0, c1 + w1))
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f (c0 + w0, c1 + w1))