internlm/Lean-Github huggingface dataset:
Theorem: fast_products_converge
Proof 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
Proof state after:
no goals
Theorem: fast_products_converge
Proof 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
Proof 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
Theorem: fast_products_converge
Proof 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 ?_
Proof 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
Theorem: fast_products_converge
Proof 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)
Proof state after:
no goals
Theorem: fast_products_converge
Proof 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
Proof 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
Theorem: fast_products_converge
Proof 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
Proof state after:
no goals
Theorem: fast_products_converge
Proof 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]
Proof state after:
no goals
Theorem: fast_products_converge
Proof 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
Proof state after:
no goals
Theorem: fast_products_converge
Proof 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
Proof 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)
Theorem: fast_products_converge
Proof 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
Proof 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)
Theorem: fast_products_converge
Proof 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
Proof 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)
Theorem: fast_products_converge
Proof 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
Proof 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)
Theorem: fast_products_converge
Proof 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]
Proof 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)
Theorem: fast_products_converge
Proof 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
Proof 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)
Theorem: fast_products_converge
Proof 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]
Proof 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)
Theorem: fast_products_converge
Proof 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
Proof state after:
no goals
Theorem: fast_products_converge
Proof 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
Proof 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
Theorem: fast_products_converge
Proof 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
Proof 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
Theorem: fast_products_converge
Proof 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
Proof 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