Theorem: superNearF (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ SuperNear (fl (f d) ∞ c) d {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
set s := superF d
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ SuperNear (fl (f d) ∞ c) d {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ SuperNear (fl (f d) ∞ c) d {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
generalize ht : {z : ℂ | abs z < (max 16 (abs c / 2))⁻¹} = t
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
⊢ SuperNear (fl (f d) ∞ c) d t

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
⊢ SuperNear (fl (f d) ∞ c) d t
Tactic:
have cz : ∀ {z}, z ∈ t → abs (c * z ^ d) ≤ 1 / 8 := by
  intro z m; simp only [← ht, mem_setOf] at m
  simp only [Complex.abs.map_mul, Complex.abs.map_pow]
  trans abs c * (max 16 (abs c / 2))⁻¹ ^ d; bound
  rw [inv_pow, mul_inv_le_iff]; swap; bound
  rw [mul_one_div]; rw [le_div_iff, mul_comm]; swap; norm_num
  refine le_trans ?_ (pow_le_pow_right (le_max_of_le_left (by norm_num)) (two_le_d d))
  by_cases cb : abs c / 2 ≤ 16
  rw [max_eq_left cb, pow_two]; linarith
  rw [max_eq_right (not_le.mp cb).le, pow_two]; nlinarith
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
⊢ SuperNear (fl (f d) ∞ c) d t

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
⊢ SuperNear (fl (f d) ∞ c) d t
Tactic:
have cz1 : ∀ {z}, z ∈ t → 7 / 8 ≤ abs (1 + c * z ^ d) := by
  intro z m
  calc abs (1 + c * z ^ d)
    _ ≥ Complex.abs 1 - abs (c * z ^ d) := by bound
    _ ≥ Complex.abs 1 - 1 / 8 := by linarith [cz m]
    _ = 7 / 8 := by norm_num
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)
⊢ SuperNear (fl (f d) ∞ c) d t

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)
⊢ SuperNear (fl (f d) ∞ c) d t
Tactic:
have zb : ∀ {z}, z ∈ t → abs z ≤ 1 / 8 := by
  intro z m; rw [← ht] at m; refine le_trans (le_of_lt m) ?_
  rw [one_div]; exact inv_le_inv_of_le (by norm_num) (le_trans (by norm_num) (le_max_left _ _))
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
⊢ SuperNear (fl (f d) ∞ c) d t

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
⊢ SuperNear (fl (f d) ∞ c) d t
Tactic:
exact
  { d2 := two_le_d d
    fa0 := (s.fla c).along_snd
    fd := fd_f
    fc := fc_f
    o := by rw [← ht]; exact isOpen_lt Complex.continuous_abs continuous_const
    t0 := by simp only [← ht, mem_setOf, Complex.abs.map_zero]; bound
    t2 := fun {z} m ↦ le_trans (zb m) (by norm_num)
    fa := by
      intro z m; rw [fl_f]
      refine ((analyticAt_id _ _).pow _).div (analyticAt_const.add
        (analyticAt_const.mul ((analyticAt_id _ _).pow _))) ?_
      rw [← Complex.abs.ne_zero_iff]; exact (lt_of_lt_of_le (by norm_num) (cz1 m)).ne'
    ft := by
      intro z m; specialize cz1 m; specialize zb m
      simp only [fl_f, mem_setOf, map_div₀, Complex.abs.map_pow, ← ht] at m ⊢
      refine lt_of_le_of_lt ?_ m; rw [div_le_iff (lt_of_lt_of_le (by norm_num) cz1)]
      refine le_trans (pow_le_pow_of_le_one (Complex.abs.nonneg _)
        (le_trans zb (by norm_num)) (two_le_d d)) ?_
      rw [pow_two]; refine mul_le_mul_of_nonneg_left ?_ (Complex.abs.nonneg _)
      exact le_trans zb (le_trans (by norm_num) cz1)
    gs' := by
      intro z z0 m; simp only [fl_f, div_div_cancel_left' (pow_ne_zero d z0)]
      specialize cz1 m
      have czp : 0 < abs (1 + c * z ^ d) := lt_of_lt_of_le (by norm_num) cz1
      refine le_of_mul_le_mul_right ?_ czp
      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]
      exact le_trans (cz m) (le_trans (by norm_num)
        (mul_le_mul_of_nonneg_left cz1 (by norm_num))) }
State after:
no goals

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
⊢ ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
Tactic:
intro z m
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
z : ℂ
m : z ∈ t
⊢ Complex.abs (c * z ^ d) ≤ 1 / 8

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
z : ℂ
m : z ∈ t
⊢ Complex.abs (c * z ^ d) ≤ 1 / 8
Tactic:
simp only [← ht, mem_setOf] at m
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs (c * z ^ d) ≤ 1 / 8

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs (c * z ^ d) ≤ 1 / 8
Tactic:
simp only [Complex.abs.map_mul, Complex.abs.map_pow]
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * Complex.abs z ^ d ≤ 1 / 8

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * Complex.abs z ^ d ≤ 1 / 8
Tactic:
trans abs c * (max 16 (abs c / 2))⁻¹ ^ d
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * Complex.abs z ^ d ≤ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d ≤ 1 / 8

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * Complex.abs z ^ d ≤ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d ≤ 1 / 8
Tactic:
bound
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d ≤ 1 / 8

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d ≤ 1 / 8
Tactic:
rw [inv_pow, mul_inv_le_iff]
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < max 16 (Complex.abs c / 2) ^ d

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < max 16 (Complex.abs c / 2) ^ d
Tactic:
swap
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < max 16 (Complex.abs c / 2) ^ d

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < max 16 (Complex.abs c / 2) ^ d

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)
Tactic:
bound
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)
Tactic:
rw [mul_one_div]
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d / 8

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d / 8
Tactic:
rw [le_div_iff, mul_comm]
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < 8

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < 8
Tactic:
swap
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < 8

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < 8

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d
Tactic:
norm_num
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d
Tactic:
refine le_trans ?_ (pow_le_pow_right (le_max_of_le_left (by norm_num)) (two_le_d d))
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Tactic:
by_cases cb : abs c / 2 ≤ 16
State after:
case pos
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2

case neg
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2

State before:
case pos
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2

case neg
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Tactic:
rw [max_eq_left cb, pow_two]
State after:
case pos
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ 16 * 16

case neg
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2

State before:
case pos
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ 16 * 16

case neg
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Tactic:
linarith
State after:
case neg
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2

State before:
case neg
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Tactic:
rw [max_eq_right (not_le.mp cb).le, pow_two]
State after:
case neg
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ Complex.abs c / 2 * (Complex.abs c / 2)

State before:
case neg
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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ Complex.abs c / 2 * (Complex.abs c / 2)
Tactic:
nlinarith
State after:
no goals

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
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 1 ≤ 16
Tactic:
norm_num
State after:
no goals

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 : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
Tactic:
intro z m
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
⊢ 7 / 8 ≤ Complex.abs (1 + c * z ^ d)

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
⊢ 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
Tactic:
calc abs (1 + c * z ^ d)
  _ ≥ Complex.abs 1 - abs (c * z ^ d) := by bound
  _ ≥ Complex.abs 1 - 1 / 8 := by linarith [cz m]
  _ = 7 / 8 := by norm_num
State after:
no goals

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
⊢ Complex.abs (1 + c * z ^ d) ≥ Complex.abs 1 - Complex.abs (c * z ^ d)
Tactic:
bound
State after:
no goals

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
⊢ Complex.abs 1 - Complex.abs (c * z ^ d) ≥ Complex.abs 1 - 1 / 8
Tactic:
linarith [cz m]
State after:
no goals

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
⊢ Complex.abs 1 - 1 / 8 = 7 / 8
Tactic:
norm_num
State after:
no goals

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)
⊢ ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
Tactic:
intro z m
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)
z : ℂ
m : z ∈ t
⊢ Complex.abs z ≤ 1 / 8

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)
z : ℂ
m : z ∈ t
⊢ Complex.abs z ≤ 1 / 8
Tactic:
rw [← ht] at m
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)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ Complex.abs z ≤ 1 / 8

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)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ Complex.abs z ≤ 1 / 8
Tactic:
refine le_trans (le_of_lt m) ?_
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)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ (max 16 (Complex.abs c / 2))⁻¹ ≤ 1 / 8

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)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ (max 16 (Complex.abs c / 2))⁻¹ ≤ 1 / 8
Tactic:
rw [one_div]
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)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ (max 16 (Complex.abs c / 2))⁻¹ ≤ 8⁻¹

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)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ (max 16 (Complex.abs c / 2))⁻¹ ≤ 8⁻¹
Tactic:
exact inv_le_inv_of_le (by norm_num) (le_trans (by norm_num) (le_max_left _ _))
State after:
no goals

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)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ 0 < 8
Tactic:
norm_num
State after:
no goals

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)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ 8 ≤ 16
Tactic:
norm_num
State after:
no goals

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
⊢ IsOpen t
Tactic:
rw [← ht]
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
⊢ IsOpen {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}

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
⊢ IsOpen {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
exact isOpen_lt Complex.continuous_abs continuous_const
State after:
no goals

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
⊢ 0 ∈ t
Tactic:
simp only [← ht, mem_setOf, Complex.abs.map_zero]
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
⊢ 0 < (max 16 (Complex.abs c / 2))⁻¹

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
⊢ 0 < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
bound
State after:
no goals

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
⊢ 1 / 8 ≤ 1 / 2
Tactic:
norm_num
State after:
no goals

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
⊢ AnalyticOn ℂ (fl (f d) ∞ c) t
Tactic:
intro z m
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
⊢ AnalyticAt ℂ (fl (f d) ∞ c) z

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
⊢ AnalyticAt ℂ (fl (f d) ∞ c) z
Tactic:
rw [fl_f]
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
⊢ AnalyticAt ℂ ((fun c z => z ^ d / (1 + c * z ^ d)) c) z

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
⊢ AnalyticAt ℂ ((fun c z => z ^ d / (1 + c * z ^ d)) c) z
Tactic:
refine ((analyticAt_id _ _).pow _).div (analyticAt_const.add
  (analyticAt_const.mul ((analyticAt_id _ _).pow _))) ?_
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
⊢ 1 + c * z ^ d ≠ 0

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
⊢ 1 + c * z ^ d ≠ 0
Tactic:
rw [← Complex.abs.ne_zero_iff]
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
⊢ Complex.abs (1 + c * z ^ d) ≠ 0

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
⊢ Complex.abs (1 + c * z ^ d) ≠ 0
Tactic:
exact (lt_of_lt_of_le (by norm_num) (cz1 m)).ne'
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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