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

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Tactic:
have c12 : (1 / 2 : ℝ) ≤ 1 / 2 := by norm_num
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Tactic:
have a0 : 0 ≤ (1 / 2 : ℝ) := by norm_num
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Tactic:
set t' := {c | (c, z) ∈ t}
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Tactic:
have o' : IsOpen t' := s.o.preimage (by continuity)
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
o' : IsOpen t'
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
o' : IsOpen t'
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Tactic:
refine (fast_products_converge' o' c12 a0 (by linarith) ?_
  fun n c m ↦ term_converges (s.ts m) n m).2.1 _ m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
o' : IsOpen t'
⊢ ∀ (n : ℕ), AnalyticOn ℂ (fun c => term (f (c, z).1) d n z) t'

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
o' : IsOpen t'
⊢ ∀ (n : ℕ), AnalyticOn ℂ (fun c => term (f (c, z).1) d n z) t'
Tactic:
exact fun n c m ↦ term_analytic_c s n m
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ 1 / 2 ≤ 1 / 2
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
⊢ 0 ≤ 1 / 2
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
⊢ Continuous fun c => (c, z)
Tactic:
continuity
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
o' : IsOpen t'
⊢ 1 / 2 < 1
Tactic:
linarith
State after:
no goals