Theorem: series2_norm (Ray/Hartogs/Osgood.lean)

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]
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

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]
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)⁻¹

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
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)⁻¹

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))‖
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)⁻¹

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
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

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
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

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)))
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

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)
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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)⁻¹

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
State after:
no goals

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
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)⁻¹

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]
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)⁻¹

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]
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)⁻¹

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
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

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
State after:
no goals