internlm/Lean-Github huggingface dataset:
Theorem: bottcherNear_lt_one
Proof state before:
case intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
b' : ∀ᶠ (n : ℕ) in atTop, Complex.abs (bottcherNear f d (f^[n] z)) < 1
n : ℕ
b : 1 ≤ Complex.abs (bottcherNear f d z)
⊢ 1 ≤ Complex.abs (bottcherNear f d (f^[n] z))
Tactic:
simp only [bottcherNear_eqn_iter s zt n, Complex.abs.map_pow, one_le_pow_of_one_le b]
Proof state after:
no goals
Theorem: bottcherNear_lt_one
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
⊢ ∀ᶠ (n : ℕ) in atTop, Complex.abs (bottcherNear f d (f^[n] z)) < 1
Tactic:
refine (Metric.tendsto_nhds.mp (iterates_tendsto s zt) r rp).mp
    (Filter.eventually_of_forall fun n h ↦ ?_)
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
n : ℕ
h : dist (f^[n] z) 0 < r
⊢ Complex.abs (bottcherNear f d (f^[n] z)) < 1
Theorem: bottcherNear_lt_one
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
n : ℕ
h : dist (f^[n] z) 0 < r
⊢ Complex.abs (bottcherNear f d (f^[n] z)) < 1
Tactic:
rw [Complex.dist_eq, sub_zero] at h
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
n : ℕ
h : Complex.abs (f^[n] z) < r
⊢ Complex.abs (bottcherNear f d (f^[n] z)) < 1
Theorem: bottcherNear_lt_one
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
n : ℕ
h : Complex.abs (f^[n] z) < r
⊢ Complex.abs (bottcherNear f d (f^[n] z)) < 1
Tactic:
exact rs h
Proof state after:
no goals
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (bottcherNear f d z) ≤ 3 * Complex.abs z
Tactic:
simp only [bottcherNear, Complex.abs.map_mul]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs z * Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3 * Complex.abs z
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs z * Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3 * Complex.abs z
Tactic:
rw [mul_comm]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (∏' (n : ℕ), term f d n z) * Complex.abs z ≤ 3 * Complex.abs z
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (∏' (n : ℕ), term f d n z) * Complex.abs z ≤ 3 * Complex.abs z
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (Complex.abs.nonneg _)
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3
Tactic:
rcases term_prod_exists s _ zt with ⟨p, h⟩
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : HasProd (fun n => term f d n z) p
⊢ Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : HasProd (fun n => term f d n z) p
⊢ Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3
Tactic:
rw [h.tprod_eq]
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : HasProd (fun n => term f d n z) p
⊢ Complex.abs p ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : HasProd (fun n => term f d n z) p
⊢ Complex.abs p ≤ 3
Tactic:
simp only [HasProd] at h
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
⊢ Complex.abs p ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
⊢ Complex.abs p ≤ 3
Tactic:
apply le_of_tendsto' (Filter.Tendsto.comp Complex.continuous_abs.continuousAt h)
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
⊢ ∀ (c : Finset ℕ), (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) c ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
⊢ ∀ (c : Finset ℕ), (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) c ≤ 3
Tactic:
intro A
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) A ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) A ≤ 3
Tactic:
clear h
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) A ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) A ≤ 3
Tactic:
simp only [Function.comp, Complex.abs.map_prod]
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Tactic:
have tb : ∀ n, abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2 : ℝ) ^ n := by
  intro n
  calc abs (term f d n z)
    _ = abs (1 + (term f d n z - 1)) := by ring_nf
    _ ≤ Complex.abs 1 + abs (term f d n z - 1) := by bound
    _ = 1 + abs (term f d n z - 1) := by norm_num
    _ ≤ 1 + 1 / 2 * (1 / 2 : ℝ) ^ n := by bound [term_converges s n zt]
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Tactic:
have p : ∀ n : ℕ, 0 < (1 : ℝ) + 1 / 2 * (1 / 2 : ℝ) ^ n := fun _ ↦ add_pos (by bound) (by bound)
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Tactic:
have lb : ∀ n : ℕ, Real.log ((1 : ℝ) + 1 / 2 * (1 / 2 : ℝ) ^ n) ≤ 1 / 2 * (1 / 2 : ℝ) ^ n :=
  fun n ↦ le_trans (Real.log_le_sub_one_of_pos (p n)) (le_of_eq (by ring))
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Tactic:
refine le_trans (Finset.prod_le_prod (fun _ _ ↦ Complex.abs.nonneg _) fun n _ ↦ tb n) ?_
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => 1 + 1 / 2 * (1 / 2) ^ i) ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => 1 + 1 / 2 * (1 / 2) ^ i) ≤ 3
Tactic:
rw [← Real.exp_log (Finset.prod_pos fun n _ ↦ p n), Real.log_prod _ _ fun n _ ↦ (p n).ne']
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => (1 + 1 / 2 * (1 / 2) ^ i).log).exp ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => (1 + 1 / 2 * (1 / 2) ^ i).log).exp ≤ 3
Tactic:
refine le_trans (Real.exp_le_exp.mpr (Finset.sum_le_sum fun n _ ↦ lb n)) ?_
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i).exp ≤ 3
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i).exp ≤ 3
Tactic:
refine le_trans (Real.exp_le_exp.mpr ?_) Real.exp_one_lt_3.le
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1
Tactic:
have geom := partial_scaled_geometric_bound (1 / 2) A one_half_pos.le one_half_lt_one
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
geom : (A.sum fun n => ↑(1 / 2) * (1 / 2) ^ n) ≤ ↑(1 / 2) * (1 - 1 / 2)⁻¹
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
geom : (A.sum fun n => ↑(1 / 2) * (1 / 2) ^ n) ≤ ↑(1 / 2) * (1 - 1 / 2)⁻¹
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1
Tactic:
simp only [NNReal.coe_div, NNReal.coe_one, NNReal.coe_two] at geom
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
geom : (A.sum fun x => 1 / 2 * (1 / 2) ^ x) ≤ 1 / 2 * (1 - 1 / 2)⁻¹
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1
Theorem: bottcherNear_le
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
geom : (A.sum fun x => 1 / 2 * (1 / 2) ^ x) ≤ 1 / 2 * (1 - 1 / 2)⁻¹
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1
Tactic:
exact le_trans geom (by norm_num)
Proof state after:
no goals
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
⊢ ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
Tactic:
intro n
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
Tactic:
calc abs (term f d n z)
  _ = abs (1 + (term f d n z - 1)) := by ring_nf
  _ ≤ Complex.abs 1 + abs (term f d n z - 1) := by bound
  _ = 1 + abs (term f d n z - 1) := by norm_num
  _ ≤ 1 + 1 / 2 * (1 / 2 : ℝ) ^ n := by bound [term_converges s n zt]
Proof state after:
no goals
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ Complex.abs (term f d n z) = Complex.abs (1 + (term f d n z - 1))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ Complex.abs (1 + (term f d n z - 1)) ≤ Complex.abs 1 + Complex.abs (term f d n z - 1)
Tactic:
bound
Proof state after:
no goals
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ Complex.abs 1 + Complex.abs (term f d n z - 1) = 1 + Complex.abs (term f d n z - 1)
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ 1 + Complex.abs (term f d n z - 1) ≤ 1 + 1 / 2 * (1 / 2) ^ n
Tactic:
bound [term_converges s n zt]
Proof state after:
no goals
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
x✝ : ℕ
⊢ 0 < 1
Tactic:
bound
Proof state after:
no goals
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
x✝ : ℕ
⊢ 0 < 1 / 2 * (1 / 2) ^ x✝
Tactic:
bound
Proof state after:
no goals
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
n : ℕ
⊢ 1 + 1 / 2 * (1 / 2) ^ n - 1 = 1 / 2 * (1 / 2) ^ n
Tactic:
ring
Proof state after:
no goals
Theorem: bottcherNear_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
geom : (A.sum fun x => 1 / 2 * (1 / 2) ^ x) ≤ 1 / 2 * (1 - 1 / 2)⁻¹
⊢ 1 / 2 * (1 - 1 / 2)⁻¹ ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: SuperNearC.ou
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ IsOpen u
Tactic:
have e : u = Prod.fst '' t := by
  ext c; simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right]
  exact ⟨fun m ↦ ⟨0, (s.s m).t0⟩, fun h ↦ Exists.elim h fun z m ↦ s.tc m⟩
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
e : u = Prod.fst '' t
⊢ IsOpen u
Theorem: SuperNearC.ou
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
e : u = Prod.fst '' t
⊢ IsOpen u
Tactic:
rw [e]
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
e : u = Prod.fst '' t
⊢ IsOpen (Prod.fst '' t)
Theorem: SuperNearC.ou
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
e : u = Prod.fst '' t
⊢ IsOpen (Prod.fst '' t)
Tactic:
exact isOpenMap_fst _ s.o
Proof state after:
no goals
Theorem: SuperNearC.ou
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ u = Prod.fst '' t
Tactic:
ext c
Proof state after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
⊢ c ∈ u ↔ c ∈ Prod.fst '' t
Theorem: SuperNearC.ou
Proof state before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
⊢ c ∈ u ↔ c ∈ Prod.fst '' t
Tactic:
simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right]
Proof state after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
⊢ c ∈ u ↔ ∃ x, (c, x) ∈ t
Theorem: SuperNearC.ou
Proof state before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
⊢ c ∈ u ↔ ∃ x, (c, x) ∈ t
Tactic:
exact ⟨fun m ↦ ⟨0, (s.s m).t0⟩, fun h ↦ Exists.elim h fun z m ↦ s.tc m⟩
Proof state after:
no goals
Theorem: SuperNearC.superAtC
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ ∀ {c : ℂ}, c ∈ u → SuperAt (f c) d
Tactic:
intro c m
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
⊢ SuperAt (f c) d
Theorem: SuperNearC.superAtC
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
⊢ SuperAt (f c) d
Tactic:
have s := s.s m
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s✝ : SuperNearC f d u t
c : ℂ
m : c ∈ u
s : SuperNear (f c) d {z | (c, z) ∈ t}
⊢ SuperAt (f c) d
Theorem: SuperNearC.superAtC
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s✝ : SuperNearC f d u t
c : ℂ
m : c ∈ u
s : SuperNear (f c) d {z | (c, z) ∈ t}
⊢ SuperAt (f c) d
Tactic:
exact
  { d2 := s.d2
    fa0 := s.fa0
    fd := s.fd
    fc := s.fc }
Proof state after:
no goals
Theorem: SuperAtC.ga_of_fa
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
⊢ AnalyticOn ℂ (g2 f d) t
Tactic:
refine Pair.hartogs o ?_ ?_
Proof state after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z0 => g2 f d (z0, c1)) c0

case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z1 => g2 f d (c0, z1)) c1
Theorem: SuperAtC.ga_of_fa
Proof state before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z0 => g2 f d (z0, c1)) c0
Tactic:
intro c z m
Proof state after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => g2 f d (z0, z)) c
Theorem: SuperAtC.ga_of_fa
Proof state before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => g2 f d (z0, z)) c
Tactic:
simp only [g2, g]
Proof state after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c
Theorem: SuperAtC.ga_of_fa
Proof state before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c
Tactic:
by_cases zero : z = 0
Proof state after:
case pos
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : z = 0
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c

case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c
Theorem: SuperAtC.ga_of_fa
Proof state before:
case pos
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : z = 0
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c
Tactic:
simp only [zero, eq_self_iff_true, if_true]
Proof state after:
case pos
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : z = 0
⊢ AnalyticAt ℂ (fun z0 => 1) c
Theorem: SuperAtC.ga_of_fa
Proof state before:
case pos
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : z = 0
⊢ AnalyticAt ℂ (fun z0 => 1) c
Tactic:
exact analyticAt_const
Proof state after:
no goals
Theorem: SuperAtC.ga_of_fa
Proof state before:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c
Tactic:
simp only [zero, if_false]
Proof state after:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => f z0 z / z ^ d) c