internlm/Lean-Github huggingface dataset:
Theorem: cauchy2_radius
Proof state before:
case h.h
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
⊢ Summable fun b_1 => (↑b_1 + 1) * b * (↑t / r) ^ b_1
Tactic:
simp_rw [mul_comm _ b, mul_assoc b _ _]
Proof state after:
case h.h
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
⊢ Summable fun b_1 => b * ((↑b_1 + 1) * (↑t / r) ^ b_1)
Theorem: cauchy2_radius
Proof state before:
case h.h
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
⊢ Summable fun b_1 => b * ((↑b_1 + 1) * (↑t / r) ^ b_1)
Tactic:
apply Summable.mul_left b
Proof state after:
case h.h
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
⊢ Summable fun i => (↑i + 1) * (↑t / r) ^ i
Theorem: cauchy2_radius
Proof state before:
case h.h
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
⊢ Summable fun i => (↑i + 1) * (↑t / r) ^ i
Tactic:
have trn : ‖↑t / r‖ < 1 := by simp; rw [abs_of_pos h.rp, div_lt_one h.rp]; assumption
Proof state after:
case h.h
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
trn : ‖↑t / r‖ < 1
⊢ Summable fun i => (↑i + 1) * (↑t / r) ^ i
Theorem: cauchy2_radius
Proof state before:
case h.h
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
trn : ‖↑t / r‖ < 1
⊢ Summable fun i => (↑i + 1) * (↑t / r) ^ i
Tactic:
simp_rw [right_distrib _ _ _, one_mul]
Proof state after:
case h.h
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
trn : ‖↑t / r‖ < 1
⊢ Summable fun i => ↑i * (↑t / r) ^ i + (↑t / r) ^ i
Theorem: cauchy2_radius
Proof state before:
case h.h
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
trn : ‖↑t / r‖ < 1
⊢ Summable fun i => ↑i * (↑t / r) ^ i + (↑t / r) ^ i
Tactic:
exact Summable.add (hasSum_coe_mul_geometric_of_norm_lt_one trn).summable
  (hasSum_geometric_of_norm_lt_one trn).summable
Proof state after:
no goals
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < r
⊢ ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
Tactic:
intro
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
t : ℝ≥0
tr : ↑t < r
n✝ : ℕ
⊢ 0 ≤ ‖series2 h n✝‖ * ↑t ^ n✝
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < r
n✝ : ℕ
⊢ 0 ≤ ‖series2 h n✝‖ * ↑t ^ n✝
Tactic:
bound
Proof state after:
no goals
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
⊢ ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ 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 : ℝ
h : Separate f c0 c1 r b s
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
n : ℕ
⊢ ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
n : ℕ
⊢ ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
Tactic:
trans (↑n + 1) * b * r⁻¹ ^ n * (t:ℝ)^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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
n : ℕ
⊢ ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * r⁻¹ ^ n * ↑t ^ n

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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
n : ℕ
⊢ (↑n + 1) * b * r⁻¹ ^ n * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
n : ℕ
⊢ ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * r⁻¹ ^ n * ↑t ^ n
Tactic:
bound [series2_norm h n]
Proof state after:
no goals
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
n : ℕ
⊢ (↑n + 1) * b * r⁻¹ ^ n * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
Tactic:
rw [mul_assoc ((↑n + 1) * b) _ _, ← mul_pow, inv_mul_eq_div]
Proof state after:
no goals
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
⊢ ‖↑t / r‖ < 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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
⊢ ↑t / |r| < 1
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
⊢ ↑t / |r| < 1
Tactic:
rw [abs_of_pos h.rp, div_lt_one h.rp]
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
⊢ ↑t < r
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < r
lo : ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
hi : ∀ (n : ℕ), ‖series2 h n‖ * ↑t ^ n ≤ (↑n + 1) * b * (↑t / r) ^ n
⊢ ↑t < r
Tactic:
assumption
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
⊢ 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
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
⊢ HasSum (fun n => w0 ^ n.2 • w1 ^ n.1 • h.series2Coeff n.2 n.1) a
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
⊢ 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
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
⊢ HasSum f a
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
⊢ HasSum f a
Tactic:
generalize hg : (fun n1 : ℕ ↦ w1 ^ n1 • h.series2CoeffN0Sum n1 w0) = 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 : ℝ
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
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
⊢ HasSum f a
Tactic:
generalize ha' : ∑' n, f n = a'
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'
⊢ HasSum f a
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'
⊢ HasSum f a
Tactic:
have gs : HasSum g a := by rw [← hg, ← ha]; exact cauchy2_hasSum_n1n0 h 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
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
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
⊢ 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
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)
⊢ HasSum f a
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:
have fs' : HasSum f a' := by rw [← ha']; exact sf.hasSum
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
fs' : HasSum f a'
⊢ HasSum f a
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
fs' : HasSum f a'
⊢ HasSum f a
Tactic:
have gs' := HasSum.prod_fiberwise fs' fs
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
fs' : HasSum f a'
gs' : HasSum (fun b => g b) a'
⊢ HasSum f a
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
fs' : HasSum f a'
gs' : HasSum (fun b => g b) a'
⊢ HasSum f a
Tactic:
rwa [HasSum.unique gs gs']
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'
⊢ HasSum g a
Tactic:
rw [← hg, ← 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'
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f✝ (c0 + w0, c1 + w1))
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'
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f✝ (c0 + w0, c1 + w1))
Tactic:
exact cauchy2_hasSum_n1n0 h w0m 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
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
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 => f (n1, n0)) (g n1)
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 => f (n1, n0)) (g n1)
Tactic:
rw [← hf, ← 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 : ℝ
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)
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 => (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
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 => w0 ^ n0 • w1 ^ n1 • h.series2Coeff n0 n1) (w1 ^ n1 • h.series2CoeffN0Sum n1 w0)