Theorem: CNonpos.degenerate (Ray/Analytic/Series.lean)

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
⊢ ∀ (n : ℕ), ∀ z ∈ s, f n z = 0
Tactic:
intro n z zs
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
n : ℕ
z : ℂ
zs : z ∈ s
⊢ f n z = 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z) ≤ c * a ^ n
n : ℕ
z : ℂ
zs : z ∈ s
⊢ f n z = 0
Tactic:
specialize hf n z zs
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
n : ℕ
z : ℂ
zs : z ∈ s
hf : Complex.abs (f n z) ≤ c * a ^ n
⊢ f n z = 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
n : ℕ
z : ℂ
zs : z ∈ s
hf : Complex.abs (f n z) ≤ c * a ^ n
⊢ f n z = 0
Tactic:
have ca : c * a ^ n ≤ 0 := mul_nonpos_iff.mpr (Or.inr ⟨c0, by bound⟩)
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
n : ℕ
z : ℂ
zs : z ∈ s
hf : Complex.abs (f n z) ≤ c * a ^ n
ca : c * a ^ n ≤ 0
⊢ f n z = 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
n : ℕ
z : ℂ
zs : z ∈ s
hf : Complex.abs (f n z) ≤ c * a ^ n
ca : c * a ^ n ≤ 0
⊢ f n z = 0
Tactic:
exact Complex.abs.eq_zero.mp (le_antisymm (le_trans hf ca) (Complex.abs.nonneg _))
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
c0 : c ≤ 0
a0 : 0 ≤ a
n : ℕ
z : ℂ
zs : z ∈ s
hf : Complex.abs (f n z) ≤ c * a ^ n
⊢ 0 ≤ a ^ n
Tactic:
bound
State after:
no goals