internlm/Lean-Github huggingface dataset:
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ 2 ^ 2 ≤ x
Tactic:
norm_num
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ 4 ≤ x
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ 4 ≤ x
Tactic:
exact x4.le
Proof state after:
no goals
Theorem: lower_anti
Proof state before:
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
⊢ 0 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: lower_anti
Proof state before:
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ 0 < x ^ (1 + p)
Tactic:
positivity
Proof state after:
no goals
Theorem: lower_anti
Proof state before:
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ 1 + p + -2 = p - 1
Tactic:
ring_nf
Proof state after:
no goals
Theorem: lower_anti
Proof state before:
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ 1 / 2 ≤ p - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: lower_anti
Proof state before:
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ 1 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: lower_anti
Proof state before:
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: lower_anti
Proof state before:
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
⊢ 0.216 ≤ ⋯.potential c ↑z
Tactic:
set s := superF 2
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
⊢ 0.216 ≤ s.potential c ↑z
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
⊢ 0.216 ≤ s.potential c ↑z
Tactic:
by_cases m : (c,↑z) ∈ s.basin
Proof state after:
case pos
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
⊢ 0.216 ≤ s.potential c ↑z

case neg
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∉ s.basin
⊢ 0.216 ≤ s.potential c ↑z
Theorem: le_potential
Proof state before:
case pos
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
⊢ 0.216 ≤ s.potential c ↑z
Tactic:
rcases pass_through c4 z4 m with ⟨n,w4,w20⟩
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w4 : 4 < Complex.abs ((f' 2 c)^[n + 1] z)
w20 : Complex.abs ((f' 2 c)^[n + 1] z) ≤ 20
⊢ 0.216 ≤ s.potential c ↑z
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w4 : 4 < Complex.abs ((f' 2 c)^[n + 1] z)
w20 : Complex.abs ((f' 2 c)^[n + 1] z) ≤ 20
⊢ 0.216 ≤ s.potential c ↑z
Tactic:
generalize hw : (f' 2 c)^[n+1] z = w at w4 w20
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
⊢ 0.216 ≤ s.potential c ↑z
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
⊢ 0.216 ≤ s.potential c ↑z
Tactic:
have cw : abs c ≤ abs w := by linarith
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
⊢ 0.216 ≤ s.potential c ↑z
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
⊢ 0.216 ≤ s.potential c ↑z
Tactic:
have pw : 0.0469 ≤ s.potential c w := by
  have pw := (abs_le.mp (le_trans (potential_approx 2 w4.le cw)
    (potential_error_le_of_z4 2 w4.le cw))).1
  rw [le_sub_iff_add_le, neg_add_eq_sub] at pw
  have anti := lower_anti 0.8095 1.864 (by norm_num) (by norm_num)
    (a := abs w) (b := 20) w4.le (by norm_num) w20
  refine le_trans ?_ (le_trans anti pw)
  norm_num
  have le : (266 : ℝ) ≤ 20 ^ (233 / 125 : ℝ) := by
    rw [div_eq_mul_inv, Real.rpow_mul (by positivity), Real.le_rpow_inv_iff_of_pos (by norm_num)
      (by positivity) (by positivity)]
    norm_num
  exact le_trans (by norm_num) (sub_le_sub_left (div_le_div_of_nonneg_left (by norm_num)
    (by norm_num) le) _)
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
⊢ 0.216 ≤ s.potential c ↑z
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
⊢ 0.216 ≤ s.potential c ↑z
Tactic:
have pwz : s.potential c w = s.potential c z ^ 2^(n+1) := by
  simp only [←hw, ←f_f'_iter, s.potential_eqn_iter]
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w = s.potential c ↑z ^ 2 ^ (n + 1)
⊢ 0.216 ≤ s.potential c ↑z
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w = s.potential c ↑z ^ 2 ^ (n + 1)
⊢ 0.216 ≤ s.potential c ↑z
Tactic:
rw [←Real.rpow_natCast] at pwz
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w = s.potential c ↑z ^ ↑(2 ^ (n + 1))
⊢ 0.216 ≤ s.potential c ↑z
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w = s.potential c ↑z ^ ↑(2 ^ (n + 1))
⊢ 0.216 ≤ s.potential c ↑z
Tactic:
rw [←Real.rpow_inv_eq s.potential_nonneg s.potential_nonneg
  (NeZero.natCast_ne (2^(n+1)) ℝ)] at pwz
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ≤ s.potential c ↑z
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ≤ s.potential c ↑z
Tactic:
rw [←pwz]
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ≤ s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ≤ s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹
Tactic:
refine le_trans ?_ (Real.rpow_le_rpow (by norm_num) pw (by positivity))
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ≤ 469e-4 ^ (↑(2 ^ (n + 1)))⁻¹
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ≤ 469e-4 ^ (↑(2 ^ (n + 1)))⁻¹
Tactic:
rw [Real.le_rpow_inv_iff_of_pos (by norm_num) (by norm_num) (by positivity), Real.rpow_natCast]
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ^ 2 ^ (n + 1) ≤ 469e-4
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ^ 2 ^ (n + 1) ≤ 469e-4
Tactic:
refine le_trans (pow_le_pow_of_le_one (by norm_num) (by norm_num)
  (pow_le_pow_right (by norm_num) (Nat.le_add_left 1 n))) ?_
Proof state after:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ^ 2 ^ 1 ≤ 469e-4
Theorem: le_potential
Proof state before:
case pos.intro.intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ^ 2 ^ 1 ≤ 469e-4
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
⊢ Complex.abs c ≤ Complex.abs w
Tactic:
linarith
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
⊢ 469e-4 ≤ s.potential c ↑w
Tactic:
have pw := (abs_le.mp (le_trans (potential_approx 2 w4.le cw)
  (potential_error_le_of_z4 2 w4.le cw))).1
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : -(0.8095 / Complex.abs w ^ 1.864) ≤ ⋯.potential c ↑w - 1 / Complex.abs w
⊢ 469e-4 ≤ s.potential c ↑w
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : -(0.8095 / Complex.abs w ^ 1.864) ≤ ⋯.potential c ↑w - 1 / Complex.abs w
⊢ 469e-4 ≤ s.potential c ↑w
Tactic:
rw [le_sub_iff_add_le, neg_add_eq_sub] at pw
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
⊢ 469e-4 ≤ s.potential c ↑w
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
⊢ 469e-4 ≤ s.potential c ↑w
Tactic:
have anti := lower_anti 0.8095 1.864 (by norm_num) (by norm_num)
  (a := abs w) (b := 20) w4.le (by norm_num) w20
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 469e-4 ≤ s.potential c ↑w
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 469e-4 ≤ s.potential c ↑w
Tactic:
refine le_trans ?_ (le_trans anti pw)
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 469e-4 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) 20
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 469e-4 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) 20
Tactic:
norm_num
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 469 / 10000 ≤ 1 / 20 - 1619 / 2000 / 20 ^ (233 / 125)
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 469 / 10000 ≤ 1 / 20 - 1619 / 2000 / 20 ^ (233 / 125)
Tactic:
have le : (266 : ℝ) ≤ 20 ^ (233 / 125 : ℝ) := by
  rw [div_eq_mul_inv, Real.rpow_mul (by positivity), Real.le_rpow_inv_iff_of_pos (by norm_num)
    (by positivity) (by positivity)]
  norm_num
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
le : 266 ≤ 20 ^ (233 / 125)
⊢ 469 / 10000 ≤ 1 / 20 - 1619 / 2000 / 20 ^ (233 / 125)
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
le : 266 ≤ 20 ^ (233 / 125)
⊢ 469 / 10000 ≤ 1 / 20 - 1619 / 2000 / 20 ^ (233 / 125)
Tactic:
exact le_trans (by norm_num) (sub_le_sub_left (div_le_div_of_nonneg_left (by norm_num)
  (by norm_num) le) _)
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
⊢ 0.8095 * 1.864 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
⊢ 3 / 2 ≤ 1.864
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
⊢ 20 ∈ Ici 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 266 ≤ 20 ^ (233 / 125)
Tactic:
rw [div_eq_mul_inv, Real.rpow_mul (by positivity), Real.le_rpow_inv_iff_of_pos (by norm_num)
  (by positivity) (by positivity)]
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 266 ^ 125 ≤ 20 ^ 233
Theorem: le_potential
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
n : ℕ
w : ℂ
hw : (f' 2 c)^[n + 1] z = w
w4 : 4 < Complex.abs w
w20 : Complex.abs w ≤ 20
cw : Complex.abs c ≤ Complex.abs w
pw : 1 / Complex.abs w - 0.8095 / Complex.abs w ^ 1.864 ≤ ⋯.potential c ↑w
anti : (fun x => 1 / x - 0.8095 / x ^ 1.864) 20 ≤ (fun x => 1 / x - 0.8095 / x ^ 1.864) (Complex.abs w)
⊢ 266 ^ 125 ≤ 20 ^ 233
Tactic:
norm_num
Proof state after:
no goals