internlm/Lean-Github huggingface dataset:
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 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))
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
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))
a : E
ha : f (c0 + w0, c1 + w1) = a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
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 x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x)
    (f (c0 + w0, c1 + w1))
a : E
ha : f (c0 + w0, c1 + w1) = a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
Tactic:
rw [ha] 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
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
ha : f (c0 + w0, c1 + w1) = a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
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
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
ha : f (c0 + w0, c1 + w1) = a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
Tactic:
clear 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
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
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
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
Tactic:
have e : (fun n ↦
    (Finset.range (n + 1)).sum fun n1 ↦ w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    fun n ↦ series2 h n fun _ : Fin n ↦ (w0, w1) := by
  clear sum; funext n
  rw [series2]; simp only [ge_iff_le, ContinuousMultilinearMap.sum_apply]
  simp_rw [termCmmap_apply]
  nth_rw 1 [← Finset.sum_range_reflect]; simp
  apply Finset.sum_congr rfl
  intro n0 n0n'; simp only [Finset.mem_range] at n0n'
  have n0n := Nat.le_of_lt_succ n0n'
  rw [Nat.sub_sub_self n0n, min_eq_left n0n]
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
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
e :
  (fun n => (Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n =>
    (series2 h n) fun x => (w0, w1)
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
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
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
e :
  (fun n => (Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n =>
    (series2 h n) fun x => (w0, w1)
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
Tactic:
rwa [←e]
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
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
⊢ (fun n => (Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n =>
    (series2 h n) fun x => (w0, w1)
Tactic:
clear 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
a : E
⊢ (fun n => (Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n =>
    (series2 h n) fun x => (w0, 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
a : E
⊢ (fun n => (Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n =>
    (series2 h n) fun x => (w0, w1)
Tactic:
funext n
Proof state after:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (series2 h n) fun x => (w0, w1)
Theorem: cauchy2_hasSum
Proof state before:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (series2 h n) fun x => (w0, w1)
Tactic:
rw [series2]
Proof state after:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    ((Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))) fun x => (w0, w1)
Theorem: cauchy2_hasSum
Proof state before:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    ((Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))) fun x => (w0, w1)
Tactic:
simp only [ge_iff_le, ContinuousMultilinearMap.sum_apply]
Proof state after:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (Finset.range (n + 1)).sum fun a => (termCmmap ℂ n a (h.series2Coeff a (n - a))) fun x => (w0, w1)
Theorem: cauchy2_hasSum
Proof state before:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (Finset.range (n + 1)).sum fun a => (termCmmap ℂ n a (h.series2Coeff a (n - a))) fun x => (w0, w1)
Tactic:
simp_rw [termCmmap_apply]
Proof state after:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Theorem: cauchy2_hasSum
Proof state before:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Tactic:
nth_rw 1 [← Finset.sum_range_reflect]
Proof state after:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun j =>
      w0 ^ (n - (n + 1 - 1 - j)) • w1 ^ (n + 1 - 1 - j) • h.series2Coeff (n - (n + 1 - 1 - j)) (n + 1 - 1 - j)) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Theorem: cauchy2_hasSum
Proof state before:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun j =>
      w0 ^ (n - (n + 1 - 1 - j)) • w1 ^ (n + 1 - 1 - j) • h.series2Coeff (n - (n + 1 - 1 - j)) (n + 1 - 1 - j)) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Tactic:
simp
Proof state after:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun x => w0 ^ (n - (n - x)) • w1 ^ (n - x) • h.series2Coeff (n - (n - x)) (n - x)) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Theorem: cauchy2_hasSum
Proof state before:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun x => w0 ^ (n - (n - x)) • w1 ^ (n - x) • h.series2Coeff (n - (n - x)) (n - x)) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    w0 ^ (n - (n - x)) • w1 ^ (n - x) • h.series2Coeff (n - (n - x)) (n - x) =
      w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Theorem: cauchy2_hasSum
Proof state before:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    w0 ^ (n - (n - x)) • w1 ^ (n - x) • h.series2Coeff (n - (n - x)) (n - x) =
      w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Tactic:
intro n0 n0n'
Proof state after:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 ∈ Finset.range (n + 1)
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)
Theorem: cauchy2_hasSum
Proof state before:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 ∈ Finset.range (n + 1)
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)
Tactic:
simp only [Finset.mem_range] at n0n'
Proof state after:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 < n + 1
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)
Theorem: cauchy2_hasSum
Proof state before:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 < n + 1
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)
Tactic:
have n0n := Nat.le_of_lt_succ n0n'
Proof state after:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 < n + 1
n0n : n0 ≤ n
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)
Theorem: cauchy2_hasSum
Proof state before:
case 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
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 < n + 1
n0n : n0 ≤ n
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)
Tactic:
rw [Nat.sub_sub_self n0n, min_eq_left n0n]
Proof state after:
no goals
Theorem: osgood_h
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
⊢ 0 < ENNReal.ofReal r
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
⊢ 0 < r
Theorem: osgood_h
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
⊢ 0 < r
Tactic:
exact h.rp
Proof state after:
no goals
Theorem: osgood_h
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
⊢ ∀ {y : ℂ × ℂ}, y ∈ EMetric.ball 0 (ENNReal.ofReal r) → HasSum (fun n => (series2 h n) fun x => y) (f ((c0, c1) + y))
Tactic:
simp only [Metric.emetric_ball, Metric.mem_ball, dist_zero_right, Prod.forall]
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 b_1 : ℂ), ‖(a, b_1)‖ < r → HasSum (fun n => (series2 h n) fun x => (a, b_1)) (f ((c0, c1) + (a, b_1)))
Theorem: osgood_h
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 b_1 : ℂ), ‖(a, b_1)‖ < r → HasSum (fun n => (series2 h n) fun x => (a, b_1)) (f ((c0, c1) + (a, b_1)))
Tactic:
intro w0 w1 wr
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
w0 w1 : ℂ
wr : ‖(w0, w1)‖ < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Theorem: osgood_h
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
w0 w1 : ℂ
wr : ‖(w0, w1)‖ < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Tactic:
rw [Prod.norm_def] at wr
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
w0 w1 : ℂ
wr : max ‖(w0, w1).1‖ ‖(w0, w1).2‖ < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Theorem: osgood_h
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
w0 w1 : ℂ
wr : max ‖(w0, w1).1‖ ‖(w0, w1).2‖ < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Tactic:
simp only [Complex.norm_eq_abs, ge_iff_le, max_lt_iff] at wr
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Theorem: osgood_h
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Tactic:
have w0m : w0 ∈ ball (0 : ℂ) r := by simp; exact wr.left
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Theorem: osgood_h
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Tactic:
have w1m : w1 ∈ ball (0 : ℂ) r := by simp; exact wr.right
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Theorem: osgood_h
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f ((c0, c1) + (w0, w1)))
Tactic:
exact cauchy2_hasSum h w0m w1m
Proof state after:
no goals
Theorem: osgood_h
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
⊢ w0 ∈ ball 0 r
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
⊢ Complex.abs w0 < r
Theorem: osgood_h
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
⊢ Complex.abs w0 < r
Tactic:
exact wr.left
Proof state after:
no goals
Theorem: osgood_h
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
⊢ w1 ∈ ball 0 r
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
⊢ Complex.abs w1 < r
Theorem: osgood_h
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
w0 w1 : ℂ
wr : Complex.abs w0 < r ∧ Complex.abs w1 < r
w0m : w0 ∈ ball 0 r
⊢ Complex.abs w1 < r
Tactic:
exact wr.right
Proof state after:
no goals
Theorem: osgood
Proof state before:
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
⊢ AnalyticOn ℂ f s
Tactic:
intro c cs
Proof state after:
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Theorem: osgood
Proof state before:
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Tactic:
rcases Metric.isOpen_iff.mp o c cs with ⟨r, rp, rs⟩
Proof state after:
case intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
⊢ AnalyticAt ℂ f c