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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ProdExistsOn (term f d) t ∧ AnalyticOn ℂ (tprodOn (term f d)) t ∧ ∀ z ∈ t, tprodOn (term f d) z ≠ 0
Tactic:
have c12 : (1 / 2 : ℝ) ≤ 1 / 2 := by norm_num
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
⊢ ProdExistsOn (term f d) t ∧ AnalyticOn ℂ (tprodOn (term f d)) t ∧ ∀ z ∈ t, tprodOn (term f d) z ≠ 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
⊢ ProdExistsOn (term f d) t ∧ AnalyticOn ℂ (tprodOn (term f d)) t ∧ ∀ z ∈ t, tprodOn (term f d) z ≠ 0
Tactic:
have a0 : 0 ≤ (1 / 2 : ℝ) := by norm_num
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
⊢ ProdExistsOn (term f d) t ∧ AnalyticOn ℂ (tprodOn (term f d)) t ∧ ∀ z ∈ t, tprodOn (term f d) z ≠ 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
⊢ ProdExistsOn (term f d) t ∧ AnalyticOn ℂ (tprodOn (term f d)) t ∧ ∀ z ∈ t, tprodOn (term f d) z ≠ 0
Tactic:
exact fast_products_converge' s.o c12 a0 (by linarith) (term_analytic s)
  fun n z ↦ term_converges s n
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ 1 / 2 ≤ 1 / 2
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
⊢ 0 ≤ 1 / 2
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
⊢ 1 / 2 < 1
Tactic:
linarith
State after:
no goals