Theorem: le_potential (Ray/Dynamics/Multibrot/PotentialLower.lean)

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
⊢ 0.216 ≤ ⋯.potential c ↑z
Tactic:
set s := superF 2
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

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
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

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⟩
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

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
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

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
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

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) _)
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

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]
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

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
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

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
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

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]
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)))⁻¹

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))
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)))⁻¹

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]
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

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))) ?_
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
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

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)
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

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
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)

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
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)

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) _)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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)]
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

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
State after:
no goals

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)
⊢ 0 ≤ 20
Tactic:
positivity
State after:
no goals

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)
⊢ 0 ≤ 266
Tactic:
norm_num
State after:
no goals

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)
⊢ 0 ≤ 20 ^ 233
Tactic:
positivity
State after:
no goals

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)
⊢ 0 < 125
Tactic:
positivity
State after:
no goals

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 / 266
Tactic:
norm_num
State after:
no goals

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)
⊢ 0 ≤ 1619 / 2000
Tactic:
norm_num
State after:
no goals

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)
⊢ 0 < 266
Tactic:
norm_num
State after:
no goals

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 : 469e-4 ≤ s.potential c ↑w
⊢ s.potential c ↑w = s.potential c ↑z ^ 2 ^ (n + 1)
Tactic:
simp only [←hw, ←f_f'_iter, s.potential_eqn_iter]
State after:
no goals

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 : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0 ≤ 469e-4
Tactic:
norm_num
State after:
no goals

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 : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0 ≤ (↑(2 ^ (n + 1)))⁻¹
Tactic:
positivity
State after:
no goals

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 : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0 ≤ 0.216
Tactic:
norm_num
State after:
no goals

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 : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0 < ↑(2 ^ (n + 1))
Tactic:
positivity
State after:
no goals

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 : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 0.216 ≤ 1
Tactic:
norm_num
State after:
no goals

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 : 469e-4 ≤ s.potential c ↑w
pwz : s.potential c ↑w ^ (↑(2 ^ (n + 1)))⁻¹ = s.potential c ↑z
⊢ 1 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
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
Tactic:
rw [s.potential_eq_one (not_exists.mp m)]
State after:
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 ≤ 1

State before:
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 ≤ 1
Tactic:
norm_num
State after:
no goals