Theorem: fast_series_converge_uniformly_on (Ray/Analytic/Series.lean)

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ HasUniformSum f (tsumOn f) s
Tactic:
by_cases c0 : c ≤ 0
State after:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
⊢ HasUniformSum f (tsumOn f) s

case neg
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : ¬c ≤ 0
⊢ HasUniformSum f (tsumOn f) s

State before:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
⊢ HasUniformSum f (tsumOn f) s
Tactic:
have fz := CNonpos.degenerate c0 a0 hf
State after:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
⊢ HasUniformSum f (tsumOn f) s

State before:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
⊢ HasUniformSum f (tsumOn f) s
Tactic:
rw [HasUniformSum, Metric.tendstoUniformlyOn_iff]
State after:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
⊢ ∀ ε > 0, ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < ε

State before:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
⊢ ∀ ε > 0, ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < ε
Tactic:
intro e ep
State after:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e

State before:
case pos
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e
Tactic:
apply Filter.eventually_of_forall
State after:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
⊢ ∀ (x : Finset ℕ), ∀ x_1 ∈ s, dist (tsumOn f x_1) (x.sum fun n => f n x_1) < e

State before:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
⊢ ∀ (x : Finset ℕ), ∀ x_1 ∈ s, dist (tsumOn f x_1) (x.sum fun n => f n x_1) < e
Tactic:
intro n z zs
State after:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (tsumOn f z) (n.sum fun n => f n z) < e

State before:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (tsumOn f z) (n.sum fun n => f n z) < e
Tactic:
rw [tsumOn]
State after:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), f n z) (n.sum fun n => f n z) < e

State before:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), f n z) (n.sum fun n => f n z) < e
Tactic:
simp_rw [fz _ z zs]
State after:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), 0) (n.sum fun n => 0) < e

State before:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), 0) (n.sum fun n => 0) < e
Tactic:
simp only [tsum_zero, Finset.sum_const_zero, dist_zero_left, Complex.norm_eq_abs,
  AbsoluteValue.map_zero]
State after:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ 0 < e

State before:
case pos.hp
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : c ≤ 0
fz : ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
e : ℝ
ep : e > 0
n : Finset ℕ
z : ℂ
zs : z ∈ s
⊢ 0 < e
Tactic:
assumption
State after:
no goals

State before:
case neg
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : ¬c ≤ 0
⊢ HasUniformSum f (tsumOn f) s
Tactic:
simp only [not_le] at c0
State after:
case neg
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
⊢ HasUniformSum f (tsumOn f) s

State before:
case neg
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
⊢ HasUniformSum f (tsumOn f) s
Tactic:
apply uniformVanishing_to_tendsto_uniformly_on
State after:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
⊢ UniformVanishing f s

State before:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
⊢ UniformVanishing f s
Tactic:
intro e ep
State after:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e

State before:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
set t := (1 - ↑a) / ↑c * (e / 2)
State after:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e

State before:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
have tp : t > 0 := by bound
State after:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e

State before:
case neg.h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
rcases exists_pow_lt_of_lt_one tp a1 with ⟨n, nt⟩
State after:
case neg.h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e

State before:
case neg.h.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
⊢ ∃ n, ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
use n
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
⊢ ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
⊢ ∀ (N : Finset ℕ) (z : ℂ), Late N n → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
intro N z NL zs
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
⊢ (N.sum fun n => Complex.abs (f n z)) < e

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
⊢ (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
have a1p : 1 - (a : ℝ) > 0 := by linarith
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ (N.sum fun n => Complex.abs (f n z)) < e

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ (N.sum fun n => Complex.abs (f n z)) < e
Tactic:
calc (N.sum fun n ↦ abs (f n z))
  _ ≤ N.sum fun n ↦ c * a ^ n := Finset.sum_le_sum fun n _ ↦ hf n z zs
  _ = c * N.sum fun n ↦ a ^ n := (Finset.mul_sum _ _ _).symm
  _ ≤ c * (a ^ n * (1 - a)⁻¹) := by bound [late_geometric_bound NL a0 a1]
  _ = a ^ n * (c * (1 - a)⁻¹) := by ring
  _ ≤ t * (c * (1 - a)⁻¹) := by bound
  _ = (1 - a) / c * (e / 2) * (c * (1 - a)⁻¹) := rfl
  _ = (1 - a) * (1 - a)⁻¹ * (c / c) * (e / 2) := by ring
  _ = 1 * 1 * (e / 2) := by rw [mul_inv_cancel a1p.ne', div_self c0.ne']
  _ = e / 2 := by ring
  _ < e := by linarith
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
⊢ t > 0
Tactic:
bound
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
⊢ 1 - a > 0
Tactic:
linarith
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ (c * N.sum fun n => a ^ n) ≤ c * (a ^ n * (1 - a)⁻¹)
Tactic:
bound [late_geometric_bound NL a0 a1]
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ c * (a ^ n * (1 - a)⁻¹) = a ^ n * (c * (1 - a)⁻¹)
Tactic:
ring
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ a ^ n * (c * (1 - a)⁻¹) ≤ t * (c * (1 - a)⁻¹)
Tactic:
bound
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ (1 - a) / c * (e / 2) * (c * (1 - a)⁻¹) = (1 - a) * (1 - a)⁻¹ * (c / c) * (e / 2)
Tactic:
ring
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ (1 - a) * (1 - a)⁻¹ * (c / c) * (e / 2) = 1 * 1 * (e / 2)
Tactic:
rw [mul_inv_cancel a1p.ne', div_self c0.ne']
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ 1 * 1 * (e / 2) = e / 2
Tactic:
ring
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
a0 : 0 ≤ a
a1 : a < 1
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
c0 : 0 < c
e : ℝ
ep : e > 0
t : ℝ := (1 - a) / c * (e / 2)
tp : t > 0
n : ℕ
nt : a ^ n < t
N : Finset ℕ
z : ℂ
NL : Late N n
zs : z ∈ s
a1p : 1 - a > 0
⊢ e / 2 < e
Tactic:
linarith
State after:
no goals