Theorem: term_nonzero (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), z ∈ t → term f d n z ≠ 0
Tactic:
intro n zt
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ term f d n z ≠ 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ term f d n z ≠ 0
Tactic:
have h := term_converges s n zt
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
⊢ term f d n z ≠ 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
⊢ term f d n z ≠ 0
Tactic:
have o : 1 / 2 * (1 / 2 : ℝ) ^ n < 1 := by
  have p : (1 / 2 : ℝ) ^ n ≤ 1 := pow_le_one n (by norm_num) (by linarith)
  calc
    1 / 2 * (1 / 2 : ℝ) ^ n ≤ 1 / 2 * 1 := by linarith
    _ < 1 := by norm_num
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
o : 1 / 2 * (1 / 2) ^ n < 1
⊢ term f d n z ≠ 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
o : 1 / 2 * (1 / 2) ^ n < 1
⊢ term f d n z ≠ 0
Tactic:
exact near_one_avoids_zero (lt_of_le_of_lt h o)
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 1 / 2 * (1 / 2) ^ n < 1
Tactic:
have p : (1 / 2 : ℝ) ^ n ≤ 1 := pow_le_one n (by norm_num) (by linarith)
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
p : (1 / 2) ^ n ≤ 1
⊢ 1 / 2 * (1 / 2) ^ n < 1

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
p : (1 / 2) ^ n ≤ 1
⊢ 1 / 2 * (1 / 2) ^ n < 1
Tactic:
calc
  1 / 2 * (1 / 2 : ℝ) ^ n ≤ 1 / 2 * 1 := by linarith
  _ < 1 := by norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 0 ≤ 1 / 2
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 1 / 2 ≤ 1
Tactic:
linarith
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
p : (1 / 2) ^ n ≤ 1
⊢ 1 / 2 * (1 / 2) ^ n ≤ 1 / 2 * 1
Tactic:
linarith
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
p : (1 / 2) ^ n ≤ 1
⊢ 1 / 2 * 1 < 1
Tactic:
norm_num
State after:
no goals