internlm/Lean-Github huggingface dataset:
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 ℕ
⊢ (N.sum fun n => fl n z).exp = N.prod fun n => f n z
Tactic:
rw [Complex.exp_sum]
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.prod fun x => (fl x z).exp) = 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 ℕ
⊢ (N.prod fun x => (fl x z).exp) = N.prod fun n => f n z
Tactic:
simp_rw [expfl _ z zs]
Proof state after:
no goals
Theorem: fast_products_converge
Proof 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]
Proof 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
Theorem: fast_products_converge
Proof 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)
Proof state after:
no goals
Theorem: fast_products_converge
Proof 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]
Proof state after:
no goals
Theorem: fast_products_converge'
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
⊢ ProdExistsOn f s ∧ AnalyticOn ℂ (tprodOn f) s ∧ ∀ z ∈ s, tprodOn f z ≠ 0
Tactic:
rcases fast_products_converge o c12 a0 a1 h hf with ⟨g, gp, ga, g0⟩
Proof state after:
case intro.intro.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ProdExistsOn f s ∧ AnalyticOn ℂ (tprodOn f) s ∧ ∀ z ∈ s, tprodOn f z ≠ 0
Theorem: fast_products_converge'
Proof state before:
case intro.intro.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ProdExistsOn f s ∧ AnalyticOn ℂ (tprodOn f) s ∧ ∀ z ∈ s, tprodOn f z ≠ 0
Tactic:
refine ⟨?_, ?_, ?_⟩
Proof state after:
case intro.intro.intro.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ProdExistsOn f s

case intro.intro.intro.refine_2
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ AnalyticOn ℂ (tprodOn f) s

case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ∀ z ∈ s, tprodOn f z ≠ 0
Theorem: fast_products_converge'
Proof state before:
case intro.intro.intro.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ProdExistsOn f s
Tactic:
exact fun z zs ↦ ⟨g z, gp z zs⟩
Proof state after:
no goals
Theorem: fast_products_converge'
Proof state before:
case intro.intro.intro.refine_2
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ AnalyticOn ℂ (tprodOn f) s
Tactic:
rwa [← analyticOn_congr o fun z zs ↦ (gp.tprodOn_eq z zs).symm]
Proof state after:
no goals
Theorem: fast_products_converge'
Proof state before:
case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ∀ z ∈ s, tprodOn f z ≠ 0
Tactic:
intro z zs
Proof state after:
case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
z : ℂ
zs : z ∈ s
⊢ tprodOn f z ≠ 0
Theorem: fast_products_converge'
Proof state before:
case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
z : ℂ
zs : z ∈ s
⊢ tprodOn f z ≠ 0
Tactic:
rw [gp.tprodOn_eq z zs]
Proof state after:
case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
z : ℂ
zs : z ∈ s
⊢ g z ≠ 0
Theorem: fast_products_converge'
Proof state before:
case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
z : ℂ
zs : z ∈ s
⊢ g z ≠ 0
Tactic:
exact g0 z zs
Proof state after:
no goals
Theorem: product_pow
Proof state before:
f : ℕ → ℂ
g : ℂ
p : ℕ
h : HasProd f g
⊢ HasProd (fun n => f n ^ p) (g ^ p)
Tactic:
rw [HasProd]
Proof state after:
f : ℕ → ℂ
g : ℂ
p : ℕ
h : HasProd f g
⊢ Filter.Tendsto (fun s => s.prod fun b => f b ^ p) atTop (𝓝 (g ^ p))
Theorem: product_pow
Proof state before:
f : ℕ → ℂ
g : ℂ
p : ℕ
h : HasProd f g
⊢ Filter.Tendsto (fun s => s.prod fun b => f b ^ p) atTop (𝓝 (g ^ p))
Tactic:
simp_rw [Finset.prod_pow]
Proof state after:
f : ℕ → ℂ
g : ℂ
p : ℕ
h : HasProd f g
⊢ Filter.Tendsto (fun s => (s.prod fun x => f x) ^ p) atTop (𝓝 (g ^ p))
Theorem: product_pow
Proof state before:
f : ℕ → ℂ
g : ℂ
p : ℕ
h : HasProd f g
⊢ Filter.Tendsto (fun s => (s.prod fun x => f x) ^ p) atTop (𝓝 (g ^ p))
Tactic:
exact Filter.Tendsto.comp (Continuous.tendsto (continuous_pow p) g) h
Proof state after:
no goals
Theorem: product_pow'
Proof state before:
f : ℕ → ℂ
p : ℕ
h : ProdExists f
⊢ tprod f ^ p = ∏' (n : ℕ), f n ^ p
Tactic:
rcases h with ⟨g, h⟩
Proof state after:
case intro
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ tprod f ^ p = ∏' (n : ℕ), f n ^ p
Theorem: product_pow'
Proof state before:
case intro
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ tprod f ^ p = ∏' (n : ℕ), f n ^ p
Tactic:
rw [HasProd.tprod_eq h]
Proof state after:
case intro
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ g ^ p = ∏' (n : ℕ), f n ^ p
Theorem: product_pow'
Proof state before:
case intro
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ g ^ p = ∏' (n : ℕ), f n ^ p
Tactic:
rw [HasProd.tprod_eq _]
Proof state after:
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ HasProd (fun n => f n ^ p) (g ^ p)
Theorem: product_pow'
Proof state before:
f : ℕ → ℂ
p : ℕ
g : ℂ
h : HasProd f g
⊢ HasProd (fun n => f n ^ p) (g ^ p)
Tactic:
exact product_pow p h
Proof state after:
no goals
Theorem: product_cons
Proof state before:
a g : ℂ
f : ℕ → ℂ
h : HasProd f g
⊢ HasProd (Stream'.cons a f) (a * g)
Tactic:
rw [HasProd] at h ⊢
Proof state after:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Theorem: product_cons
Proof state before:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Tactic:
have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_mul_left a) g) h
Proof state after:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Theorem: product_cons
Proof state before:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Tactic:
have s : ((fun z ↦ a * z) ∘ fun N : Finset ℕ ↦ N.prod f) =
    (fun N : Finset ℕ ↦ N.prod (Stream'.cons a f)) ∘ push := by
  apply funext; intro N; simp; exact push_prod
Proof state after:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
s : ((fun z => a * z) ∘ fun N => N.prod f) = (fun N => N.prod (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Theorem: product_cons
Proof state before:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
s : ((fun z => a * z) ∘ fun N => N.prod f) = (fun N => N.prod (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Tactic:
rw [s] at ha
Proof state after:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun N => N.prod (Stream'.cons a f)) ∘ push) atTop (𝓝 (a * g))
s : ((fun z => a * z) ∘ fun N => N.prod f) = (fun N => N.prod (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Theorem: product_cons
Proof state before:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun N => N.prod (Stream'.cons a f)) ∘ push) atTop (𝓝 (a * g))
s : ((fun z => a * z) ∘ fun N => N.prod f) = (fun N => N.prod (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.prod fun b => Stream'.cons a f b) atTop (𝓝 (a * g))
Tactic:
exact tendsto_comp_push.mp ha
Proof state after:
no goals
Theorem: product_cons
Proof state before:
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
⊢ ((fun z => a * z) ∘ fun N => N.prod f) = (fun N => N.prod (Stream'.cons a f)) ∘ push
Tactic:
apply funext
Proof state after:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
⊢ ∀ (x : Finset ℕ), ((fun z => a * z) ∘ fun N => N.prod f) x = ((fun N => N.prod (Stream'.cons a f)) ∘ push) x
Theorem: product_cons
Proof state before:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
⊢ ∀ (x : Finset ℕ), ((fun z => a * z) ∘ fun N => N.prod f) x = ((fun N => N.prod (Stream'.cons a f)) ∘ push) x
Tactic:
intro N
Proof state after:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
N : Finset ℕ
⊢ ((fun z => a * z) ∘ fun N => N.prod f) N = ((fun N => N.prod (Stream'.cons a f)) ∘ push) N
Theorem: product_cons
Proof state before:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
N : Finset ℕ
⊢ ((fun z => a * z) ∘ fun N => N.prod f) N = ((fun N => N.prod (Stream'.cons a f)) ∘ push) N
Tactic:
simp
Proof state after:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
N : Finset ℕ
⊢ a * N.prod f = (push N).prod (Stream'.cons a f)
Theorem: product_cons
Proof state before:
case h
a g : ℂ
f : ℕ → ℂ
h : Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a * b) ∘ fun s => s.prod fun b => f b) atTop (𝓝 (a * g))
N : Finset ℕ
⊢ a * N.prod f = (push N).prod (Stream'.cons a f)
Tactic:
exact push_prod
Proof state after:
no goals
Theorem: product_cons'
Proof state before:
a : ℂ
f : ℕ → ℂ
h : ProdExists f
⊢ tprod (Stream'.cons a f) = a * tprod f
Tactic:
rcases h with ⟨g, h⟩
Proof state after:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ tprod (Stream'.cons a f) = a * tprod f
Theorem: product_cons'
Proof state before:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ tprod (Stream'.cons a f) = a * tprod f
Tactic:
rw [HasProd.tprod_eq h]
Proof state after:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ tprod (Stream'.cons a f) = a * g
Theorem: product_cons'
Proof state before:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ tprod (Stream'.cons a f) = a * g
Tactic:
rw [HasProd.tprod_eq _]
Proof state after:
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ HasProd (fun b => Stream'.cons a f b) (a * g)
Theorem: product_cons'
Proof state before:
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasProd f g
⊢ HasProd (fun b => Stream'.cons a f b) (a * g)
Tactic:
exact product_cons h
Proof state after:
no goals
Theorem: product_drop
Proof state before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
⊢ HasProd (fun n => f (n + 1)) (g / f 0)
Tactic:
have c := @product_cons (f 0)⁻¹ _ _ h
Proof state after:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : HasProd (Stream'.cons (f 0)⁻¹ f) ((f 0)⁻¹ * g)
⊢ HasProd (fun n => f (n + 1)) (g / f 0)
Theorem: product_drop
Proof state before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : HasProd (Stream'.cons (f 0)⁻¹ f) ((f 0)⁻¹ * g)
⊢ HasProd (fun n => f (n + 1)) (g / f 0)
Tactic:
rw [HasProd]
Proof state after:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : HasProd (Stream'.cons (f 0)⁻¹ f) ((f 0)⁻¹ * g)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Theorem: product_drop
Proof state before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : HasProd (Stream'.cons (f 0)⁻¹ f) ((f 0)⁻¹ * g)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Tactic:
rw [inv_mul_eq_div, HasProd, ← tendsto_comp_push, ← tendsto_comp_push] at c
Proof state after:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (((fun s => s.prod fun b => Stream'.cons (f 0)⁻¹ f b) ∘ push) ∘ push) atTop (𝓝 (g / f 0))
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Theorem: product_drop
Proof state before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (((fun s => s.prod fun b => Stream'.cons (f 0)⁻¹ f b) ∘ push) ∘ push) atTop (𝓝 (g / f 0))
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Tactic:
have s : ((fun N : Finset ℕ ↦ N.prod fun n ↦ (Stream'.cons (f 0)⁻¹ f) n) ∘ push) ∘ push =
    fun N : Finset ℕ ↦ N.prod fun n ↦ f (n + 1) := by
  clear c h g; apply funext; intro N; simp
  nth_rw 2 [← Stream'.eta f]
  simp only [←push_prod, Stream'.head, Stream'.tail, Stream'.get, ←mul_assoc, inv_mul_cancel f0,
    one_mul]
Proof state after:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (((fun s => s.prod fun b => Stream'.cons (f 0)⁻¹ f b) ∘ push) ∘ push) atTop (𝓝 (g / f 0))
s : ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Theorem: product_drop
Proof state before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (((fun s => s.prod fun b => Stream'.cons (f 0)⁻¹ f b) ∘ push) ∘ push) atTop (𝓝 (g / f 0))
s : ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Tactic:
rw [s] at c
Proof state after:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (fun N => N.prod fun n => f (n + 1)) atTop (𝓝 (g / f 0))
s : ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Theorem: product_drop
Proof state before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (fun N => N.prod fun n => f (n + 1)) atTop (𝓝 (g / f 0))
s : ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.prod fun b => f (b + 1)) atTop (𝓝 (g / f 0))
Tactic:
assumption
Proof state after:
no goals
Theorem: product_drop
Proof state before:
f : ℕ → ℂ
g : ℂ
f0 : f 0 ≠ 0
h : HasProd f g
c : Filter.Tendsto (((fun s => s.prod fun b => Stream'.cons (f 0)⁻¹ f b) ∘ push) ∘ push) atTop (𝓝 (g / f 0))
⊢ ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
Tactic:
clear c h g
Proof state after:
f : ℕ → ℂ
f0 : f 0 ≠ 0
⊢ ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
Theorem: product_drop
Proof state before:
f : ℕ → ℂ
f0 : f 0 ≠ 0
⊢ ((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push = fun N => N.prod fun n => f (n + 1)
Tactic:
apply funext
Proof state after:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
⊢ ∀ (x : Finset ℕ), (((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push) x = x.prod fun n => f (n + 1)
Theorem: product_drop
Proof state before:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
⊢ ∀ (x : Finset ℕ), (((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push) x = x.prod fun n => f (n + 1)
Tactic:
intro N
Proof state after:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ (((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push) N = N.prod fun n => f (n + 1)
Theorem: product_drop
Proof state before:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ (((fun N => N.prod fun n => Stream'.cons (f 0)⁻¹ f n) ∘ push) ∘ push) N = N.prod fun n => f (n + 1)
Tactic:
simp
Proof state after:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ ((push (push N)).prod fun n => Stream'.cons (f 0)⁻¹ f n) = N.prod fun n => f (n + 1)
Theorem: product_drop
Proof state before:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ ((push (push N)).prod fun n => Stream'.cons (f 0)⁻¹ f n) = N.prod fun n => f (n + 1)
Tactic:
nth_rw 2 [← Stream'.eta f]
Proof state after:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ ((push (push N)).prod fun n => Stream'.cons (f 0)⁻¹ (Stream'.cons (Stream'.head f) (Stream'.tail f)) n) =
    N.prod fun n => f (n + 1)
Theorem: product_drop
Proof state before:
case h
f : ℕ → ℂ
f0 : f 0 ≠ 0
N : Finset ℕ
⊢ ((push (push N)).prod fun n => Stream'.cons (f 0)⁻¹ (Stream'.cons (Stream'.head f) (Stream'.tail f)) n) =
    N.prod fun n => f (n + 1)
Tactic:
simp only [←push_prod, Stream'.head, Stream'.tail, Stream'.get, ←mul_assoc, inv_mul_cancel f0,
  one_mul]
Proof state after:
no goals
Theorem: product_drop'
Proof state before:
f : ℕ → ℂ
f0 : f 0 ≠ 0
h : ProdExists f
⊢ ∏' (n : ℕ), f (n + 1) = tprod f / f 0
Tactic:
rcases h with ⟨g, h⟩
Proof state after:
case intro
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ ∏' (n : ℕ), f (n + 1) = tprod f / f 0