internlm/Lean-Github huggingface dataset:
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ 0 < 7 / 8
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ MapsTo (fl (f d) ∞ c) t t
Tactic:
intro z m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ fl (f d) ∞ c z ∈ t
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ fl (f d) ∞ c z ∈ t
Tactic:
specialize cz1 m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
⊢ fl (f d) ∞ c z ∈ t
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
⊢ fl (f d) ∞ c z ∈ t
Tactic:
specialize zb m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
⊢ fl (f d) ∞ c z ∈ t
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
⊢ fl (f d) ∞ c z ∈ t
Tactic:
simp only [fl_f, mem_setOf, map_div₀, Complex.abs.map_pow, ← ht] at m ⊢
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z ^ d / Complex.abs (1 + c * z ^ d) < (max 16 (Complex.abs c / 2))⁻¹
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z ^ d / Complex.abs (1 + c * z ^ d) < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
refine lt_of_le_of_lt ?_ m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z ^ d / Complex.abs (1 + c * z ^ d) ≤ Complex.abs z
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z ^ d / Complex.abs (1 + c * z ^ d) ≤ Complex.abs z
Tactic:
rw [div_le_iff (lt_of_lt_of_le (by norm_num) cz1)]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z ^ d ≤ Complex.abs z * Complex.abs (1 + c * z ^ d)
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z ^ d ≤ Complex.abs z * Complex.abs (1 + c * z ^ d)
Tactic:
refine le_trans (pow_le_pow_of_le_one (Complex.abs.nonneg _)
  (le_trans zb (by norm_num)) (two_le_d d)) ?_
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z ^ 2 ≤ Complex.abs z * Complex.abs (1 + c * z ^ d)
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z ^ 2 ≤ Complex.abs z * Complex.abs (1 + c * z ^ d)
Tactic:
rw [pow_two]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z * Complex.abs z ≤ Complex.abs z * Complex.abs (1 + c * z ^ d)
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z * Complex.abs z ≤ Complex.abs z * Complex.abs (1 + c * z ^ d)
Tactic:
refine mul_le_mul_of_nonneg_left ?_ (Complex.abs.nonneg _)
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z ≤ Complex.abs (1 + c * z ^ d)
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs z ≤ Complex.abs (1 + c * z ^ d)
Tactic:
exact le_trans zb (le_trans (by norm_num) cz1)
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < 7 / 8
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 1 / 8 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : Complex.abs z ≤ 1 / 8
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 1 / 8 ≤ 7 / 8
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ ∀ {z : ℂ}, z ≠ 0 → z ∈ t → Complex.abs (fl (f d) ∞ c z / z ^ d - 1) ≤ 1 / 4
Tactic:
intro z z0 m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
⊢ Complex.abs (fl (f d) ∞ c z / z ^ d - 1) ≤ 1 / 4
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
⊢ Complex.abs (fl (f d) ∞ c z / z ^ d - 1) ≤ 1 / 4
Tactic:
simp only [fl_f, div_div_cancel_left' (pow_ne_zero d z0)]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
⊢ Complex.abs ((1 + c * z ^ d)⁻¹ - 1) ≤ 1 / 4
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
⊢ Complex.abs ((1 + c * z ^ d)⁻¹ - 1) ≤ 1 / 4
Tactic:
specialize cz1 m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
⊢ Complex.abs ((1 + c * z ^ d)⁻¹ - 1) ≤ 1 / 4
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
⊢ Complex.abs ((1 + c * z ^ d)⁻¹ - 1) ≤ 1 / 4
Tactic:
have czp : 0 < abs (1 + c * z ^ d) := lt_of_lt_of_le (by norm_num) cz1
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
czp : 0 < Complex.abs (1 + c * z ^ d)
⊢ Complex.abs ((1 + c * z ^ d)⁻¹ - 1) ≤ 1 / 4
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
czp : 0 < Complex.abs (1 + c * z ^ d)
⊢ Complex.abs ((1 + c * z ^ d)⁻¹ - 1) ≤ 1 / 4
Tactic:
refine le_of_mul_le_mul_right ?_ czp
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
czp : 0 < Complex.abs (1 + c * z ^ d)
⊢ Complex.abs ((1 + c * z ^ d)⁻¹ - 1) * Complex.abs (1 + c * z ^ d) ≤ 1 / 4 * Complex.abs (1 + c * z ^ d)
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
czp : 0 < Complex.abs (1 + c * z ^ d)
⊢ Complex.abs ((1 + c * z ^ d)⁻¹ - 1) * Complex.abs (1 + c * z ^ d) ≤ 1 / 4 * Complex.abs (1 + c * z ^ d)
Tactic:
rw [← Complex.abs.map_mul, mul_sub_right_distrib, one_mul,
  inv_mul_cancel (Complex.abs.ne_zero_iff.mp czp.ne'), ← sub_sub, sub_self, zero_sub,
  Complex.abs.map_neg]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
czp : 0 < Complex.abs (1 + c * z ^ d)
⊢ Complex.abs (c * z ^ d) ≤ 1 / 4 * Complex.abs (1 + c * z ^ d)
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
czp : 0 < Complex.abs (1 + c * z ^ d)
⊢ Complex.abs (c * z ^ d) ≤ 1 / 4 * Complex.abs (1 + c * z ^ d)
Tactic:
exact le_trans (cz m) (le_trans (by norm_num)
  (mul_le_mul_of_nonneg_left cz1 (by norm_num)))
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
⊢ 0 < 7 / 8
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
czp : 0 < Complex.abs (1 + c * z ^ d)
⊢ 1 / 8 ≤ 1 / 4 * (7 / 8)
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
z0 : z ≠ 0
m : z ∈ t
cz1 : 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
czp : 0 < Complex.abs (1 + c * z ^ d)
⊢ 0 ≤ 1 / 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: critical_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ Critical (f d c) z ↔ z = 0 ∨ z = ∞
Tactic:
induction' z using OnePoint.rec with z
Proof state after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Critical (f d c) ∞ ↔ ∞ = 0 ∨ ∞ = ∞

case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ Critical (f d c) ↑z ↔ ↑z = 0 ∨ ↑z = ∞
Theorem: critical_f
Proof state before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Critical (f d c) ∞ ↔ ∞ = 0 ∨ ∞ = ∞
Tactic:
simp only [(superF d).critical_a, or_true]
Proof state after:
no goals
Theorem: critical_f
Proof state before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ Critical (f d c) ↑z ↔ ↑z = 0 ∨ ↑z = ∞
Tactic:
have zx : ∀ x : ℂ, (0 : ℂ →L[ℂ] ℂ) x = 0 := fun x ↦ ContinuousLinearMap.zero_apply _
Proof state after:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ Critical (f d c) ↑z ↔ ↑z = 0 ∨ ↑z = ∞
Theorem: critical_f
Proof state before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ Critical (f d c) ↑z ↔ ↑z = 0 ∨ ↑z = ∞
Tactic:
simp only [Critical, mfderiv, (holomorphicF (c, z)).along_snd.mdifferentiableAt, if_pos,
  ModelWithCorners.Boundaryless.range_eq_univ, fderivWithin_univ, writtenInExtChartAt_coe_f,
  RiemannSphere.extChartAt_coe, coePartialEquiv_symm_apply, toComplex_coe, coe_eq_zero,
  coe_eq_inf_iff, or_false_iff, ← deriv_fderiv, deriv_f', ContinuousLinearMap.ext_iff,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, Algebra.id.smul_eq_mul,
  one_mul, mul_eq_zero, Nat.cast_eq_zero, d_ne_zero, false_or_iff,
  pow_eq_zero_iff (d_minus_one_pos d).ne', zx]
Proof state after:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ (∀ (x : ℂ), x = 0 ∨ z = 0) ↔ z = 0
Theorem: critical_f
Proof state before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ (∀ (x : ℂ), x = 0 ∨ z = 0) ↔ z = 0
Tactic:
constructor
Proof state after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ (∀ (x : ℂ), x = 0 ∨ z = 0) → z = 0

case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ z = 0 → ∀ (x : ℂ), x = 0 ∨ z = 0
Theorem: critical_f
Proof state before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ (∀ (x : ℂ), x = 0 ∨ z = 0) → z = 0
Tactic:
intro h
Proof state after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : ∀ (x : ℂ), x = 0 ∨ z = 0
⊢ z = 0
Theorem: critical_f
Proof state before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : ∀ (x : ℂ), x = 0 ∨ z = 0
⊢ z = 0
Tactic:
specialize h 1
Proof state after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : 1 = 0 ∨ z = 0
⊢ z = 0
Theorem: critical_f
Proof state before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : 1 = 0 ∨ z = 0
⊢ z = 0
Tactic:
simp only [one_mul, mul_eq_zero, one_ne_zero, false_or_iff] at h
Proof state after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : z = 0
⊢ z = 0
Theorem: critical_f
Proof state before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : z = 0
⊢ z = 0
Tactic:
exact h
Proof state after:
no goals
Theorem: critical_f
Proof state before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ z = 0 → ∀ (x : ℂ), x = 0 ∨ z = 0
Tactic:
exact fun h x ↦ Or.inr h
Proof state after:
no goals
Theorem: multibrot_basin'
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ c ∈ multibrot d ↔ (c, ↑c) ∉ ⋯.basin
Tactic:
simp only [multibrot, mem_setOf, Super.basin_iff_attracts, Attracts]
Proof state after:
no goals
Theorem: multibrot_basin
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ c ∈ multibrot d ↔ (c, 0) ∉ ⋯.basin
Tactic:
set s := superF d
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ c ∈ multibrot d ↔ (c, 0) ∉ s.basin
Theorem: multibrot_basin
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ c ∈ multibrot d ↔ (c, 0) ∉ s.basin
Tactic:
simp only [multibrot_basin', not_iff_not, Super.basin, mem_setOf]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ (∃ n, (c, (f d c)^[n] ↑c) ∈ ⋯.near) ↔ ∃ n, (c, (f d c)^[n] 0) ∈ s.near
Theorem: multibrot_basin
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n] ↑c) ∈ ⋯.near) ↔ ∃ n, (c, (f d c)^[n] 0) ∈ s.near
Tactic:
simp only [e]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near) ↔ ∃ n, (c, (f d c)^[n] 0) ∈ s.near
Theorem: multibrot_basin
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near) ↔ ∃ n, (c, (f d c)^[n] 0) ∈ s.near
Tactic:
constructor
Proof state after:
case mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near) → ∃ n, (c, (f d c)^[n] 0) ∈ s.near

case mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n] 0) ∈ s.near) → ∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near
Theorem: multibrot_basin
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
Tactic:
intro n
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
n : ℕ
⊢ (f d c)^[n] ↑c = (f d c)^[n + 1] 0