Theorem: cauchy2_radius (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
⊢ ENNReal.ofReal r ≤ (series2 h).radius
Tactic:
apply ENNReal.le_of_forall_nnreal_lt
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

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

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

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

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

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

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

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

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

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

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

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

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

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
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
t : ℝ≥0
tr : ↑t < r
⊢ ∀ (n : ℕ), 0 ≤ ‖series2 h n‖ * ↑t ^ n
Tactic:
intro
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✝

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

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

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

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

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