Theorem: fast_products_converge (Ray/Analytic/Products.lean)

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
set fl := fun n z ↦ log (f n z)
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
have near1 : ∀ n z, z ∈ s → abs (f n z - 1) ≤ 1 / 2 := by
  intro n z zs
  calc abs (f n z - 1)
    _ ≤ c * a ^ n := hf n z zs
    _ ≤ (1 / 2 : ℝ) * (1:ℝ) ^ n := by bound
    _ = 1 / 2 := by norm_num
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
have near1' : ∀ n z, z ∈ s → abs (f n z - 1) < 1 := fun n z zs ↦
  lt_of_le_of_lt (near1 n z zs) (by linarith)
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
have expfl : ∀ n z, z ∈ s → exp (fl n z) = f n z := by
  intro n z zs; refine Complex.exp_log ?_
  exact near_one_avoids_zero (near1' n z zs)
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
have hl : ∀ n, AnalyticOn ℂ (fl n) s := fun n ↦
  (h n).log (fun z m ↦ mem_slitPlane_of_near_one (near1' n z m))
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
set c2 := 2 * c
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
have hfl : ∀ n z, z ∈ s → abs (fl n z) ≤ c2 * a ^ n := by
  intro n z zs
  calc abs (fl n z)
    _ = abs (log (f n z)) := rfl
    _ ≤ 2 * abs (f n z - 1) := (log_small (near1 n z zs))
    _ ≤ 2 * (c * a ^ n) := by linarith [hf n z zs]
    _ = 2 * c * a ^ n := by ring
    _ = c2 * a ^ n := rfl
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
rcases fast_series_converge o a0 a1 hl hfl with ⟨gl, gla, us⟩
State after:
case intro.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0

State before:
case intro.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
generalize hg : (fun z ↦ exp (gl z)) = g
State after:
case intro.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0

State before:
case intro.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
use g
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
refine ⟨?_, ?_, ?_⟩
State after:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ HasProdOn f g s

case h.refine_2
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ AnalyticOn ℂ g s

case h.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ ∀ z ∈ s, g z ≠ 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
⊢ ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
Tactic:
intro n z zs
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
n : ℕ
z : ℂ
zs : z ∈ s
⊢ Complex.abs (f n z - 1) ≤ 1 / 2

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
n : ℕ
z : ℂ
zs : z ∈ s
⊢ Complex.abs (f n z - 1) ≤ 1 / 2
Tactic:
calc abs (f n z - 1)
  _ ≤ c * a ^ n := hf n z zs
  _ ≤ (1 / 2 : ℝ) * (1:ℝ) ^ n := by bound
  _ = 1 / 2 := by norm_num
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
n : ℕ
z : ℂ
zs : z ∈ s
⊢ c * a ^ n ≤ 1 / 2 * 1 ^ n
Tactic:
bound
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
n : ℕ
z : ℂ
zs : z ∈ s
⊢ 1 / 2 * 1 ^ n = 1 / 2
Tactic:
norm_num
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
n : ℕ
z : ℂ
zs : z ∈ s
⊢ 1 / 2 < 1
Tactic:
linarith
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
⊢ ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
Tactic:
intro n z zs
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
n : ℕ
z : ℂ
zs : z ∈ s
⊢ (fl n z).exp = f n z

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
n : ℕ
z : ℂ
zs : z ∈ s
⊢ (fl n z).exp = f n z
Tactic:
refine Complex.exp_log ?_
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
n : ℕ
z : ℂ
zs : z ∈ s
⊢ f n z ≠ 0

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
n : ℕ
z : ℂ
zs : z ∈ s
⊢ f n z ≠ 0
Tactic:
exact near_one_avoids_zero (near1' n z zs)
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
⊢ ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
Tactic:
intro n z zs
State after:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
n : ℕ
z : ℂ
zs : z ∈ s
⊢ Complex.abs (fl n z) ≤ c2 * a ^ n

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
n : ℕ
z : ℂ
zs : z ∈ s
⊢ Complex.abs (fl n z) ≤ c2 * a ^ n
Tactic:
calc abs (fl n z)
  _ = abs (log (f n z)) := rfl
  _ ≤ 2 * abs (f n z - 1) := (log_small (near1 n z zs))
  _ ≤ 2 * (c * a ^ n) := by linarith [hf n z zs]
  _ = 2 * c * a ^ n := by ring
  _ = c2 * a ^ n := rfl
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
n : ℕ
z : ℂ
zs : z ∈ s
⊢ 2 * Complex.abs (f n z - 1) ≤ 2 * (c * a ^ n)
Tactic:
linarith [hf n z zs]
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
n : ℕ
z : ℂ
zs : z ∈ s
⊢ 2 * (c * a ^ n) = 2 * c * a ^ n
Tactic:
ring
State after:
no goals

State before:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ HasProdOn f g s
Tactic:
intro z zs
State after:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
⊢ HasProd (fun n => f n z) (g z)

State before:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
⊢ HasProd (fun n => f n z) (g z)
Tactic:
specialize us z zs
State after:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => (fun n => fl n) n z) (gl z)
⊢ HasProd (fun n => f n z) (g z)

State before:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => (fun n => fl n) n z) (gl z)
⊢ HasProd (fun n => f n z) (g z)
Tactic:
simp at us
State after:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
⊢ HasProd (fun n => f n z) (g z)

State before:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
⊢ HasProd (fun n => f n z) (g z)
Tactic:
have comp :
  Filter.Tendsto (exp ∘ fun N : Finset ℕ ↦ N.sum fun n ↦ fl n z) atTop (𝓝 (exp (gl z))) :=
  Filter.Tendsto.comp (Continuous.tendsto Complex.continuous_exp _) us
State after:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
⊢ HasProd (fun n => f n z) (g z)

State before:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
⊢ HasProd (fun n => f n z) (g z)
Tactic:
have expsum0 : (exp ∘ fun N : Finset ℕ ↦ N.sum fun n ↦ fl n z) = fun N : Finset ℕ ↦
    N.prod fun n ↦ f n z := by
  apply funext; intro N; simp; rw [Complex.exp_sum]; simp_rw [expfl _ z zs]
State after:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
expsum0 : (exp ∘ fun N => N.sum fun n => fl n z) = fun N => N.prod fun n => f n z
⊢ HasProd (fun n => f n z) (g z)

State before:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
expsum0 : (exp ∘ fun N => N.sum fun n => fl n z) = fun N => N.prod fun n => f n z
⊢ HasProd (fun n => f n z) (g z)
Tactic:
rw [expsum0] at comp
State after:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (fun N => N.prod fun n => f n z) atTop (𝓝 (gl z).exp)
expsum0 : (exp ∘ fun N => N.sum fun n => fl n z) = fun N => N.prod fun n => f n z
⊢ HasProd (fun n => f n z) (g z)

State before:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (fun N => N.prod fun n => f n z) atTop (𝓝 (gl z).exp)
expsum0 : (exp ∘ fun N => N.sum fun n => fl n z) = fun N => N.prod fun n => f n z
⊢ HasProd (fun n => f n z) (g z)
Tactic:
rw [← hg]
State after:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (fun N => N.prod fun n => f n z) atTop (𝓝 (gl z).exp)
expsum0 : (exp ∘ fun N => N.sum fun n => fl n z) = fun N => N.prod fun n => f n z
⊢ HasProd (fun n => f n z) ((fun z => (gl z).exp) z)

State before:
case h.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (fun N => N.prod fun n => f n z) atTop (𝓝 (gl z).exp)
expsum0 : (exp ∘ fun N => N.sum fun n => fl n z) = fun N => N.prod fun n => f n z
⊢ HasProd (fun n => f n z) ((fun z => (gl z).exp) z)
Tactic:
assumption
State after:
no goals

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
⊢ (exp ∘ fun N => N.sum fun n => fl n z) = fun N => N.prod fun n => f n z
Tactic:
apply funext
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
⊢ ∀ (x : Finset ℕ), (exp ∘ fun N => N.sum fun n => fl n z) x = x.prod fun n => f n z

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
⊢ ∀ (x : Finset ℕ), (exp ∘ fun N => N.sum fun n => fl n z) x = x.prod fun n => f n z
Tactic:
intro N
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
N : Finset ℕ
⊢ (exp ∘ fun N => N.sum fun n => fl n z) N = N.prod fun n => f n z

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
N : Finset ℕ
⊢ (exp ∘ fun N => N.sum fun n => fl n z) N = N.prod fun n => f n z
Tactic:
simp
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
N : Finset ℕ
⊢ (N.sum fun n => fl n z).exp = N.prod fun n => f n z

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
N : Finset ℕ
⊢ (N.sum fun n => fl n z).exp = N.prod fun n => f n z
Tactic:
rw [Complex.exp_sum]
State after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
N : Finset ℕ
⊢ (N.prod fun x => (fl x z).exp) = N.prod fun n => f n z

State before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
z : ℂ
zs : z ∈ s
us : HasSum (fun n => fl n z) (gl z)
comp : Filter.Tendsto (exp ∘ fun N => N.sum fun n => fl n z) atTop (𝓝 (gl z).exp)
N : Finset ℕ
⊢ (N.prod fun x => (fl x z).exp) = N.prod fun n => f n z
Tactic:
simp_rw [expfl _ z zs]
State after:
no goals

State before:
case h.refine_2
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ AnalyticOn ℂ g s
Tactic:
rw [← hg]
State after:
case h.refine_2
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ AnalyticOn ℂ (fun z => (gl z).exp) s

State before:
case h.refine_2
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ AnalyticOn ℂ (fun z => (gl z).exp) s
Tactic:
exact fun z zs ↦ AnalyticAt.exp.comp (gla z zs)
State after:
no goals

State before:
case h.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
a c : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : a ≥ 0
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
fl : ℕ → ℂ → ℂ := fun n z => (f n z).log
near1 : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
near1' : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) < 1
expfl : ∀ (n : ℕ), ∀ z ∈ s, (fl n z).exp = f n z
hl : ∀ (n : ℕ), AnalyticOn ℂ (fl n) s
c2 : ℝ := 2 * c
hfl : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (fl n z) ≤ c2 * a ^ n
gl : ℂ → ℂ
gla : AnalyticOn ℂ gl s
us : HasSumOn (fun n => fl n) gl s
g : ℂ → ℂ
hg : (fun z => (gl z).exp) = g
⊢ ∀ z ∈ s, g z ≠ 0
Tactic:
simp only [Complex.exp_ne_zero, Ne, not_false_iff, imp_true_iff, ← hg]
State after:
no goals