internlm/Lean-Github huggingface dataset:
Theorem: series2Coeff_bound
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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Tactic:
rw [Separate.series2Coeff]
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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖(2 * ↑π * I)⁻¹ •
        ∮ (z0 : ℂ) in C(c0, r),
          (z0 - c0)⁻¹ ^ n0 •
            (z0 - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)
Theorem: series2Coeff_bound
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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖(2 * ↑π * I)⁻¹ •
        ∮ (z0 : ℂ) in C(c0, r),
          (z0 - c0)⁻¹ ^ n0 •
            (z0 - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)
Tactic:
rw [e] at outer
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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖(2 * ↑π * I)⁻¹ •
        ∮ (z0 : ℂ) in C(c0, r),
          (z0 - c0)⁻¹ ^ n0 •
            (z0 - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)
Theorem: series2Coeff_bound
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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖(2 * ↑π * I)⁻¹ •
        ∮ (z0 : ℂ) in C(c0, r),
          (z0 - c0)⁻¹ ^ n0 •
            (z0 - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)
Tactic:
exact outer
Proof state after:
no goals
Theorem: series2Coeff_bound
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
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
⊢ b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
Tactic:
rw [mul_assoc, ← pow_add, add_comm n0 _]
Proof state after:
no goals
Theorem: series2_norm
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
n : ℕ
⊢ ‖series2 h n‖ ≤ (↑n + 1) * b * r⁻¹ ^ n
Tactic:
rw [series2]
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
n : ℕ
⊢ ‖(Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ (↑n + 1) * b * r⁻¹ ^ n
Theorem: series2_norm
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
n : ℕ
⊢ ‖(Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ (↑n + 1) * b * r⁻¹ ^ n
Tactic:
simp only [ge_iff_le, 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
n : ℕ
⊢ ‖(Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ (↑n + 1) * b * (r ^ n)⁻¹
Theorem: series2_norm
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
n : ℕ
⊢ ‖(Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ (↑n + 1) * b * (r ^ n)⁻¹
Tactic:
have tb : ∀ n0, n0 ∈ Finset.range (n+1) →
    ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n := by
  intro n0 n0n; simp at n0n
  apply le_trans (termCmmap_norm ℂ n n0 (h.series2Coeff n0 (n - n0)))
  have sb := series2Coeff_bound h n0 (n - n0)
  rw [← Nat.add_sub_assoc (Nat.le_of_lt_succ n0n) n0, Nat.add_sub_cancel_left] at sb
  assumption
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
n : ℕ
tb : ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
⊢ ‖(Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ (↑n + 1) * b * (r ^ n)⁻¹
Theorem: series2_norm
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
n : ℕ
tb : ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
⊢ ‖(Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ (↑n + 1) * b * (r ^ n)⁻¹
Tactic:
trans (Finset.range (n + 1)).sum fun n0 ↦ ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖
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
n : ℕ
tb : ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
⊢ ‖(Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤
    (Finset.range (n + 1)).sum fun n0 => ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖

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
n : ℕ
tb : ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
⊢ ((Finset.range (n + 1)).sum fun n0 => ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖) ≤ (↑n + 1) * b * (r ^ n)⁻¹
Theorem: series2_norm
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
n : ℕ
⊢ ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
Tactic:
intro n0 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
n n0 : ℕ
n0n : n0 ∈ Finset.range (n + 1)
⊢ ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
Theorem: series2_norm
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
n n0 : ℕ
n0n : n0 ∈ Finset.range (n + 1)
⊢ ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
Tactic:
simp at 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
n n0 : ℕ
n0n : n0 < n + 1
⊢ ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
Theorem: series2_norm
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
n n0 : ℕ
n0n : n0 < n + 1
⊢ ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
Tactic:
apply le_trans (termCmmap_norm ℂ n n0 (h.series2Coeff n0 (n - n0)))
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
n n0 : ℕ
n0n : n0 < n + 1
⊢ ‖h.series2Coeff n0 (n - n0)‖ ≤ b * r⁻¹ ^ n
Theorem: series2_norm
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
n n0 : ℕ
n0n : n0 < n + 1
⊢ ‖h.series2Coeff n0 (n - n0)‖ ≤ b * r⁻¹ ^ n
Tactic:
have sb := series2Coeff_bound h n0 (n - n0)
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
n n0 : ℕ
n0n : n0 < n + 1
sb : ‖h.series2Coeff n0 (n - n0)‖ ≤ b * r⁻¹ ^ (n0 + (n - n0))
⊢ ‖h.series2Coeff n0 (n - n0)‖ ≤ b * r⁻¹ ^ n
Theorem: series2_norm
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
n n0 : ℕ
n0n : n0 < n + 1
sb : ‖h.series2Coeff n0 (n - n0)‖ ≤ b * r⁻¹ ^ (n0 + (n - n0))
⊢ ‖h.series2Coeff n0 (n - n0)‖ ≤ b * r⁻¹ ^ n
Tactic:
rw [← Nat.add_sub_assoc (Nat.le_of_lt_succ n0n) n0, Nat.add_sub_cancel_left] at sb
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
n n0 : ℕ
n0n : n0 < n + 1
sb : ‖h.series2Coeff n0 (n - n0)‖ ≤ b * r⁻¹ ^ n
⊢ ‖h.series2Coeff n0 (n - n0)‖ ≤ b * r⁻¹ ^ n
Theorem: series2_norm
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
n n0 : ℕ
n0n : n0 < n + 1
sb : ‖h.series2Coeff n0 (n - n0)‖ ≤ b * r⁻¹ ^ n
⊢ ‖h.series2Coeff n0 (n - n0)‖ ≤ b * r⁻¹ ^ n
Tactic:
assumption
Proof state after:
no goals
Theorem: series2_norm
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
n : ℕ
tb : ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
⊢ ‖(Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤
    (Finset.range (n + 1)).sum fun n0 => ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖
Tactic:
bound
Proof state after:
no goals
Theorem: series2_norm
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
n : ℕ
tb : ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
⊢ ((Finset.range (n + 1)).sum fun n0 => ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖) ≤ (↑n + 1) * b * (r ^ n)⁻¹
Tactic:
trans (Finset.range (n + 1)).sum fun _ ↦ b * r⁻¹ ^ 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
n : ℕ
tb : ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
⊢ ((Finset.range (n + 1)).sum fun n0 => ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖) ≤
    (Finset.range (n + 1)).sum fun x => b * r⁻¹ ^ 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
n : ℕ
tb : ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
⊢ ((Finset.range (n + 1)).sum fun x => b * r⁻¹ ^ n) ≤ (↑n + 1) * b * (r ^ n)⁻¹
Theorem: series2_norm
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
n : ℕ
tb : ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
⊢ ((Finset.range (n + 1)).sum fun n0 => ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖) ≤
    (Finset.range (n + 1)).sum fun x => b * r⁻¹ ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: series2_norm
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
n : ℕ
tb : ∀ n0 ∈ Finset.range (n + 1), ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ ≤ b * r⁻¹ ^ n
⊢ ((Finset.range (n + 1)).sum fun x => b * r⁻¹ ^ n) ≤ (↑n + 1) * b * (r ^ n)⁻¹
Tactic:
clear tb
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
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun x => b * r⁻¹ ^ n) ≤ (↑n + 1) * b * (r ^ n)⁻¹
Theorem: series2_norm
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
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun x => b * r⁻¹ ^ n) ≤ (↑n + 1) * b * (r ^ n)⁻¹
Tactic:
rw [Finset.sum_const]
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
n : ℕ
⊢ (Finset.range (n + 1)).card • (b * r⁻¹ ^ n) ≤ (↑n + 1) * b * (r ^ n)⁻¹
Theorem: series2_norm
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
n : ℕ
⊢ (Finset.range (n + 1)).card • (b * r⁻¹ ^ n) ≤ (↑n + 1) * b * (r ^ n)⁻¹
Tactic:
simp only [Finset.card_range, inv_pow, nsmul_eq_mul, Nat.cast_add, Nat.cast_one]
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
n : ℕ
⊢ (↑n + 1) * (b * (r ^ n)⁻¹) ≤ (↑n + 1) * b * (r ^ n)⁻¹
Theorem: series2_norm
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
n : ℕ
⊢ (↑n + 1) * (b * (r ^ n)⁻¹) ≤ (↑n + 1) * b * (r ^ n)⁻¹
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
n : ℕ
⊢ ↑n * b * r⁻¹ ^ n + b * r⁻¹ ^ n ≤ ↑n * b * r⁻¹ ^ n + b * r⁻¹ ^ n
Theorem: series2_norm
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
n : ℕ
⊢ ↑n * b * r⁻¹ ^ n + b * r⁻¹ ^ n ≤ ↑n * b * r⁻¹ ^ n + b * r⁻¹ ^ n
Tactic:
rfl
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
⊢ ENNReal.ofReal r ≤ (series2 h).radius
Tactic:
apply ENNReal.le_of_forall_nnreal_lt
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
⊢ ∀ (r_1 : ℝ≥0), ↑r_1 < ENNReal.ofReal r → ↑r_1 ≤ (series2 h).radius
Theorem: cauchy2_radius
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
⊢ ∀ (r_1 : ℝ≥0), ↑r_1 < ENNReal.ofReal r → ↑r_1 ≤ (series2 h).radius
Tactic:
intro t tr
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
t : ℝ≥0
tr : ↑t < ENNReal.ofReal r
⊢ ↑t ≤ (series2 h).radius
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < ENNReal.ofReal r
⊢ ↑t ≤ (series2 h).radius
Tactic:
rw [←ENNReal.toReal_lt_toReal (@ENNReal.coe_ne_top t) (@ENNReal.ofReal_ne_top r)] at tr
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
t : ℝ≥0
tr : (↑t).toReal < (ENNReal.ofReal r).toReal
⊢ ↑t ≤ (series2 h).radius
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : (↑t).toReal < (ENNReal.ofReal r).toReal
⊢ ↑t ≤ (series2 h).radius
Tactic:
rw [ENNReal.coe_toReal, ENNReal.toReal_ofReal h.rp.le] at tr
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
t : ℝ≥0
tr : ↑t < r
⊢ ↑t ≤ (series2 h).radius
Theorem: cauchy2_radius
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
t : ℝ≥0
tr : ↑t < r
⊢ ↑t ≤ (series2 h).radius
Tactic:
apply FormalMultilinearSeries.le_radius_of_summable_nnnorm
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
⊢ Summable fun n => ‖series2 h n‖₊ * t ^ n
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
⊢ Summable fun n => ‖series2 h n‖₊ * t ^ n
Tactic:
simp_rw [← norm_toNNReal, ← NNReal.summable_coe]
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
⊢ Summable fun a => ↑(‖series2 h a‖.toNNReal * t ^ a)
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
⊢ Summable fun a => ↑(‖series2 h a‖.toNNReal * t ^ a)
Tactic:
simp
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
⊢ Summable fun a => ‖series2 h a‖ * ↑t ^ a
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
⊢ Summable fun a => ‖series2 h a‖ * ↑t ^ a
Tactic:
have lo : ∀ n : ℕ, 0 ≤ ‖series2 h n‖ * (t:ℝ)^n := by intro; bound
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
⊢ Summable fun a => ‖series2 h a‖ * ↑t ^ a
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 a => ‖series2 h a‖ * ↑t ^ a
Tactic:
refine .of_nonneg_of_le lo hi ?_
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_1 + 1) * b * (↑t / r) ^ b_1