internlm/Lean-Github huggingface dataset:
Theorem: bottcher_approx_z
Proof state before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : Tendsto (fun s => s.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) Filter.atTop (𝓝 p)
⊢ Complex.abs (p - 1) ≤ 16 * (Complex.abs z)⁻¹
Tactic:
apply le_of_tendsto' (Filter.Tendsto.comp Complex.continuous_abs.continuousAt (h.sub_const 1))
Proof state after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : Tendsto (fun s => s.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) Filter.atTop (𝓝 p)
⊢ ∀ (c_1 : Finset ℕ),
    (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) c_1 ≤ 16 * (Complex.abs z)⁻¹
Theorem: bottcher_approx_z
Proof state before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : Tendsto (fun s => s.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) Filter.atTop (𝓝 p)
⊢ ∀ (c_1 : Finset ℕ),
    (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) c_1 ≤ 16 * (Complex.abs z)⁻¹
Tactic:
clear h
Proof state after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
⊢ ∀ (c_1 : Finset ℕ),
    (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) c_1 ≤ 16 * (Complex.abs z)⁻¹
Theorem: bottcher_approx_z
Proof state before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
⊢ ∀ (c_1 : Finset ℕ),
    (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) c_1 ≤ 16 * (Complex.abs z)⁻¹
Tactic:
intro A
Proof state after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) A ≤ 16 * (Complex.abs z)⁻¹
Theorem: bottcher_approx_z
Proof state before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) A ≤ 16 * (Complex.abs z)⁻¹
Tactic:
simp only [Function.comp]
Proof state after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ Complex.abs ((A.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) ≤ 16 * (Complex.abs z)⁻¹
Theorem: bottcher_approx_z
Proof state before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ Complex.abs ((A.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) ≤ 16 * (Complex.abs z)⁻¹
Tactic:
rw [(by norm_num : (16 : ℝ) = 4 * 4), mul_assoc]
Proof state after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ Complex.abs ((A.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) ≤ 4 * (4 * (Complex.abs z)⁻¹)
Theorem: bottcher_approx_z
Proof state before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ Complex.abs ((A.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) ≤ 4 * (4 * (Complex.abs z)⁻¹)
Tactic:
refine dist_prod_one_le_abs_sum ?_ (by linarith)
Proof state after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun n => Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1)) ≤ 4 * (Complex.abs z)⁻¹
Theorem: bottcher_approx_z
Proof state before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun n => Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1)) ≤ 4 * (Complex.abs z)⁻¹
Tactic:
refine le_trans (Finset.sum_le_sum fun n _ ↦ term_approx d (by linarith) cz n) ?_
Proof state after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun i => 2 * (1 / 2) ^ i * (Complex.abs z)⁻¹) ≤ 4 * (Complex.abs z)⁻¹
Theorem: bottcher_approx_z
Proof state before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun i => 2 * (1 / 2) ^ i * (Complex.abs z)⁻¹) ≤ 4 * (Complex.abs z)⁻¹
Tactic:
simp only [mul_comm _ _⁻¹, ← mul_assoc, ← Finset.mul_sum]
Proof state after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ ((Complex.abs z)⁻¹ * 2 * A.sum fun i => (1 / 2) ^ i) ≤ (Complex.abs z)⁻¹ * 4
Theorem: bottcher_approx_z
Proof state before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ ((Complex.abs z)⁻¹ * 2 * A.sum fun i => (1 / 2) ^ i) ≤ (Complex.abs z)⁻¹ * 4
Tactic:
calc (abs z)⁻¹ * 2 * A.sum (fun n ↦ (1/2:ℝ)^n)
  _ ≤ (abs z)⁻¹ * 2 * (1 - 1 / 2)⁻¹ := by gcongr; apply partial_geometric_bound; repeat norm_num
  _ = (abs z)⁻¹ * 4 := by ring
Proof state after:
no goals
Theorem: bottcher_approx_z
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ (Complex.abs z)⁻¹ ≤ 1 / 8
Tactic:
rw [one_div]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ (Complex.abs z)⁻¹ ≤ 8⁻¹
Theorem: bottcher_approx_z
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ (Complex.abs z)⁻¹ ≤ 8⁻¹
Tactic:
apply inv_le_inv_of_le
Proof state after:
case ha
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 0 < 8

case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 8 ≤ Complex.abs z
Theorem: bottcher_approx_z
Proof state before:
case ha
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 0 < 8

case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 8 ≤ Complex.abs z
Tactic:
norm_num
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 8 ≤ Complex.abs z
Theorem: bottcher_approx_z
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 8 ≤ Complex.abs z
Tactic:
exact le_trans (by norm_num) (le_trans c16.le cz)
Proof state after:
no goals
Theorem: bottcher_approx_z
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 8 ≤ 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcher_approx_z
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 16 = 4 * 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcher_approx_z
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 4 * (Complex.abs z)⁻¹ ≤ 1 / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: bottcher_approx_z
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
n : ℕ
x✝ : n ∈ A
⊢ 16 < Complex.abs c
Tactic:
linarith
Proof state after:
no goals
Theorem: bottcher_approx_z
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ ((Complex.abs z)⁻¹ * 2 * A.sum fun n => (1 / 2) ^ n) ≤ (Complex.abs z)⁻¹ * 2 * (1 - 1 / 2)⁻¹
Tactic:
gcongr
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun n => (1 / 2) ^ n) ≤ (1 - 1 / 2)⁻¹
Theorem: bottcher_approx_z
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun n => (1 / 2) ^ n) ≤ (1 - 1 / 2)⁻¹
Tactic:
apply partial_geometric_bound
Proof state after:
case h.a0
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 0 ≤ 1 / 2

case h.a1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 1 / 2 < 1
Theorem: bottcher_approx_z
Proof state before:
case h.a0
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 0 ≤ 1 / 2

case h.a1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 1 / 2 < 1
Tactic:
repeat norm_num
Proof state after:
no goals
Theorem: bottcher_approx_z
Proof state before:
case h.a1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 1 / 2 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcher_approx_z
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (Complex.abs z)⁻¹ * 2 * (1 - 1 / 2)⁻¹ = (Complex.abs z)⁻¹ * 4
Tactic:
ring
Proof state after:
no goals
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ HasDerivAt (fun z => bottcher d (↑z)⁻¹) 1 0
Tactic:
rw [HasDerivAt, HasDerivAtFilter, bottcher, hasFDerivAtFilter_iff_isLittleO, coe_zero, inv_zero',
  fill_inf]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (fun x' => fill (bottcher' d) 0 (↑x')⁻¹ - 0 - (ContinuousLinearMap.smulRight 1 1) (x' - 0)) =o[𝓝 0] fun x' => x' - 0
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (fun x' => fill (bottcher' d) 0 (↑x')⁻¹ - 0 - (ContinuousLinearMap.smulRight 1 1) (x' - 0)) =o[𝓝 0] fun x' => x' - 0
Tactic:
simp only [sub_zero, ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
  smul_eq_mul, mul_one]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (fun x' => fill (bottcher' d) 0 (↑x')⁻¹ - x') =o[𝓝 0] fun x' => x'
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (fun x' => fill (bottcher' d) 0 (↑x')⁻¹ - x') =o[𝓝 0] fun x' => x'
Tactic:
rw [Asymptotics.isLittleO_iff]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℂ) in 𝓝 0, ‖fill (bottcher' d) 0 (↑x)⁻¹ - x‖ ≤ c * ‖x‖
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℂ) in 𝓝 0, ‖fill (bottcher' d) 0 (↑x)⁻¹ - x‖ ≤ c * ‖x‖
Tactic:
intro k k0
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖fill (bottcher' d) 0 (↑x)⁻¹ - x‖ ≤ k * ‖x‖
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖fill (bottcher' d) 0 (↑x)⁻¹ - x‖ ≤ k * ‖x‖
Tactic:
rw [Metric.eventually_nhds_iff]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∃ ε > 0, ∀ ⦃y : ℂ⦄, dist y 0 < ε → ‖fill (bottcher' d) 0 (↑y)⁻¹ - y‖ ≤ k * ‖y‖
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∃ ε > 0, ∀ ⦃y : ℂ⦄, dist y 0 < ε → ‖fill (bottcher' d) 0 (↑y)⁻¹ - y‖ ≤ k * ‖y‖
Tactic:
refine ⟨min 16⁻¹ (k / 16), by bound, ?_⟩
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∀ ⦃y : ℂ⦄, dist y 0 < min 16⁻¹ (k / 16) → ‖fill (bottcher' d) 0 (↑y)⁻¹ - y‖ ≤ k * ‖y‖
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ ∀ ⦃y : ℂ⦄, dist y 0 < min 16⁻¹ (k / 16) → ‖fill (bottcher' d) 0 (↑y)⁻¹ - y‖ ≤ k * ‖y‖
Tactic:
intro z le
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : dist z 0 < min 16⁻¹ (k / 16)
⊢ ‖fill (bottcher' d) 0 (↑z)⁻¹ - z‖ ≤ k * ‖z‖
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : dist z 0 < min 16⁻¹ (k / 16)
⊢ ‖fill (bottcher' d) 0 (↑z)⁻¹ - z‖ ≤ k * ‖z‖
Tactic:
simp only [Complex.dist_eq, sub_zero, lt_min_iff] at le
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
⊢ ‖fill (bottcher' d) 0 (↑z)⁻¹ - z‖ ≤ k * ‖z‖
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
⊢ ‖fill (bottcher' d) 0 (↑z)⁻¹ - z‖ ≤ k * ‖z‖
Tactic:
simp only [Complex.norm_eq_abs]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : z = 0
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z
Theorem: bottcher_hasDerivAt_one
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z
Tactic:
simp only [inv_coe z0, fill_coe]
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z
Theorem: bottcher_hasDerivAt_one
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z
Tactic:
have b : abs (bottcher' d z⁻¹ - z⁻¹⁻¹) ≤ (16:ℝ) * (abs z⁻¹)⁻¹ ^ 2 := bottcher_approx d ?_
Proof state after:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z⁻¹⁻¹) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z

case neg.refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ 16 < Complex.abs z⁻¹
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
⊢ min 16⁻¹ (k / 16) > 0
Tactic:
bound
Proof state after:
no goals
Theorem: bottcher_hasDerivAt_one
Proof state before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : z = 0
⊢ Complex.abs (fill (bottcher' d) 0 (↑z)⁻¹ - z) ≤ k * Complex.abs z
Tactic:
simp only [z0, coe_zero, inv_zero', fill_inf, sub_zero, Complex.abs.map_zero,
  MulZeroClass.mul_zero, le_refl]
Proof state after:
no goals
Theorem: bottcher_hasDerivAt_one
Proof state before:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z⁻¹⁻¹) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z
Tactic:
simp only [inv_inv] at b
Proof state after:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z
Theorem: bottcher_hasDerivAt_one
Proof state before:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ Complex.abs (bottcher' d z⁻¹ - z) ≤ k * Complex.abs z
Tactic:
apply le_trans b
Proof state after:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2 ≤ k * Complex.abs z
Theorem: bottcher_hasDerivAt_one
Proof state before:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2 ≤ k * Complex.abs z
Tactic:
simp only [map_inv₀, inv_inv, pow_two, ← mul_assoc]
Proof state after:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * Complex.abs z * Complex.abs z ≤ k * Complex.abs z
Theorem: bottcher_hasDerivAt_one
Proof state before:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * Complex.abs z * Complex.abs z ≤ k * Complex.abs z
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (Complex.abs.nonneg _)
Proof state after:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * Complex.abs z ≤ k
Theorem: bottcher_hasDerivAt_one
Proof state before:
case neg.refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * Complex.abs z ≤ k
Tactic:
calc 16 * abs z
  _ ≤ 16 * (k / 16) := by linarith [le.2]
  _ = k := by ring
Proof state after:
no goals
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * Complex.abs z ≤ 16 * (k / 16)
Tactic:
linarith [le.2]
Proof state after:
no goals
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
b : Complex.abs (bottcher' d z⁻¹ - z) ≤ 16 * (Complex.abs z⁻¹)⁻¹ ^ 2
⊢ 16 * (k / 16) = k
Tactic:
ring
Proof state after:
no goals
Theorem: bottcher_hasDerivAt_one
Proof state before:
case neg.refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ 16 < Complex.abs z⁻¹
Tactic:
rw [map_inv₀, lt_inv (by norm_num) (Complex.abs.pos_iff.mpr z0)]
Proof state after:
case neg.refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs z < 16⁻¹
Theorem: bottcher_hasDerivAt_one
Proof state before:
case neg.refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ Complex.abs z < 16⁻¹
Tactic:
exact le.1
Proof state after:
no goals
Theorem: bottcher_hasDerivAt_one
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
k : ℝ
k0 : 0 < k
z : ℂ
le : Complex.abs z < 16⁻¹ ∧ Complex.abs z < k / 16
z0 : ¬z = 0
⊢ 0 < 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcher_mfderiv_inf_ne_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ mfderiv I I (bottcher d) ∞ ≠ 0
Tactic:
simp only [mfderiv, (bottcherHolomorphic d _ multibrotExt_inf).mdifferentiableAt, if_pos,
  writtenInExtChartAt, bottcher_inf, extChartAt_inf, extChartAt_eq_refl, Function.comp,
  PartialEquiv.refl_coe, id, PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, invEquiv_apply,
  RiemannSphere.inv_inf, coePartialEquiv_symm_apply, toComplex_zero, PartialEquiv.coe_trans_symm,
  PartialEquiv.symm_symm, coePartialEquiv_apply, Equiv.toPartialEquiv_symm_apply, invEquiv_symm,
  ModelWithCorners.Boundaryless.range_eq_univ, fderivWithin_univ]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ fderiv ℂ (fun x => bottcher d (↑x)⁻¹) 0 ≠ 0