internlm/Lean-Github huggingface dataset:
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
case h.hp
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
e : ℂ
w : S
fm : uncurry f (e, w) ∈ (extChartAt 𝓘(ℂ, ℂ) (f c z)).source
m : (e, w) ∈ (extChartAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) (c, z)).source
⊢ ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
        (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
      (e, w) =
    (fun p => (p.1, f p.1 p.2)) (e, w)
Tactic:
simp only [Function.comp, uncurry, extChartAt_prod, PartialEquiv.prod_source, mem_prod_eq] at fm m
Proof state after:
case h.hp
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
e : ℂ
w : S
fm : f e w ∈ (extChartAt 𝓘(ℂ, ℂ) (f c z)).source
m : e ∈ (extChartAt 𝓘(ℂ, ℂ) c).source ∧ w ∈ (extChartAt 𝓘(ℂ, ℂ) z).source
⊢ ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
        (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
      (e, w) =
    (fun p => (p.1, f p.1 p.2)) (e, w)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
case h.hp
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
gn : NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
e : ℂ
w : S
fm : f e w ∈ (extChartAt 𝓘(ℂ, ℂ) (f c z)).source
m : e ∈ (extChartAt 𝓘(ℂ, ℂ) c).source ∧ w ∈ (extChartAt 𝓘(ℂ, ℂ) z).source
⊢ ((fun p => (p.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)).symm p.2)) ∘ fun x =>
        (x.1, ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f x.1 (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x.2)))))
      (e, w) =
    (fun p => (p.1, f p.1 p.2)) (e, w)
Tactic:
simp only [Function.comp, PartialEquiv.left_inv _ m.2, PartialEquiv.left_inv _ fm]
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
⊢ AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
rw [← hg]
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
⊢ AnalyticAt ℂ (uncurry fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
⊢ AnalyticAt ℂ (uncurry fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
exact (holomorphicAt_iff.mp fa).2
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ NontrivialHolomorphicAt (g c) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
rw [← hg]
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ NontrivialHolomorphicAt ((fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) c)
    (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds_param
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → S → T
c : ℂ
z : S
n : NontrivialHolomorphicAt (f c) z
fa : HolomorphicAt (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) 𝓘(ℂ, ℂ) (uncurry f) (c, z)
g : ℂ → ℂ → ℂ
hg : (fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ (uncurry g) (c, ↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ NontrivialHolomorphicAt ((fun e x => ↑(extChartAt 𝓘(ℂ, ℂ) (f c z)) (f e (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) c)
    (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
exact n.inCharts
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
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g z ≠ 0
Tactic:
set fl := fun n z ↦ log (f n z)
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
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g 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
⊢ ∃ 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
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
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g 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
⊢ ∃ 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)
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
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g 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
⊢ ∃ 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)
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
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g 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
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))
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
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g 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
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
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
⊢ ∃ g, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z ∈ s, g 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
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
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
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
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
⊢ ∃ 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⟩
Proof 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
Theorem: fast_products_converge
Proof 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
Proof 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
Theorem: fast_products_converge
Proof 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
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
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
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
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 ⟨?_, ?_, ?_⟩
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
⊢ 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
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
⊢ ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ 1 / 2
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
n : ℕ
z : ℂ
zs : z ∈ s
⊢ Complex.abs (f n z - 1) ≤ 1 / 2
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
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
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
n : ℕ
z : ℂ
zs : z ∈ s
⊢ c * a ^ n ≤ 1 / 2 * 1 ^ n
Tactic:
bound
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
n : ℕ
z : ℂ
zs : z ∈ s
⊢ 1 / 2 * 1 ^ n = 1 / 2
Tactic:
norm_num
Proof state after:
no goals