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

State before:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
⊢ AntitoneOn (fun x => 1 / x - k / x ^ p) (Ici 4)
Tactic:
have hd : ∀ x, 4 ≤ x → HasDerivAt (fun x : ℝ ↦ 1 / x - k / x^p)
    (-(x^2)⁻¹ - k * (-(p * x^(p-1)) / (x^p)^2)) x := by
  intro x x2
  simp only [one_div, div_eq_mul_inv, one_mul]
  refine (hasDerivAt_inv (by positivity)).sub (HasDerivAt.const_mul _ ?_)
  exact (Real.hasDerivAt_rpow_const (Or.inl (by positivity))).inv (by positivity)
State after:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
⊢ AntitoneOn (fun x => 1 / x - k / x ^ p) (Ici 4)

State before:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
⊢ AntitoneOn (fun x => 1 / x - k / x ^ p) (Ici 4)
Tactic:
simp only [ge_iff_le] at kp hp
State after:
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
⊢ AntitoneOn (fun x => 1 / x - k / x ^ p) (Ici 4)

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
⊢ AntitoneOn (fun x => 1 / x - k / x ^ p) (Ici 4)
Tactic:
have d : DifferentiableOn ℝ (fun x ↦ 1 / x - k / x^p) (Ici 4) :=
  fun x m ↦ (hd x m).differentiableAt.differentiableWithinAt
State after:
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)
⊢ AntitoneOn (fun x => 1 / x - k / x ^ p) (Ici 4)

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)
⊢ AntitoneOn (fun x => 1 / x - k / x ^ p) (Ici 4)
Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ici _)
State after:
case hf
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)
⊢ ContinuousOn (fun x => 1 / x - k / x ^ p) (Ici 4)

case hf'
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)
⊢ DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (interior (Ici 4))

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 ∈ interior (Ici 4), deriv (fun x => 1 / x - k / x ^ p) x ≤ 0

State before:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
⊢ ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
Tactic:
intro x x2
State after:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
x : ℝ
x2 : 4 ≤ x
⊢ HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x

State before:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
x : ℝ
x2 : 4 ≤ x
⊢ HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
Tactic:
simp only [one_div, div_eq_mul_inv, one_mul]
State after:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
x : ℝ
x2 : 4 ≤ x
⊢ HasDerivAt (fun x => x⁻¹ - k * (x ^ p)⁻¹) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) * ((x ^ p) ^ 2)⁻¹)) x

State before:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
x : ℝ
x2 : 4 ≤ x
⊢ HasDerivAt (fun x => x⁻¹ - k * (x ^ p)⁻¹) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) * ((x ^ p) ^ 2)⁻¹)) x
Tactic:
refine (hasDerivAt_inv (by positivity)).sub (HasDerivAt.const_mul _ ?_)
State after:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
x : ℝ
x2 : 4 ≤ x
⊢ HasDerivAt (fun x => (x ^ p)⁻¹) (-(p * x ^ (p - 1)) * ((x ^ p) ^ 2)⁻¹) x

State before:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
x : ℝ
x2 : 4 ≤ x
⊢ HasDerivAt (fun x => (x ^ p)⁻¹) (-(p * x ^ (p - 1)) * ((x ^ p) ^ 2)⁻¹) x
Tactic:
exact (Real.hasDerivAt_rpow_const (Or.inl (by positivity))).inv (by positivity)
State after:
no goals

State before:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
x : ℝ
x2 : 4 ≤ x
⊢ x ≠ 0
Tactic:
positivity
State after:
no goals

State before:
c z : ℂ
k p : ℝ
kp : autoParam (k * p ≤ 2) _auto✝
hp : autoParam (3 / 2 ≤ p) _auto✝
x : ℝ
x2 : 4 ≤ x
⊢ x ^ p ≠ 0
Tactic:
positivity
State after:
no goals

State before:
case hf
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)
⊢ ContinuousOn (fun x => 1 / x - k / x ^ p) (Ici 4)
Tactic:
exact d.continuousOn
State after:
no goals

State before:
case hf'
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)
⊢ DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (interior (Ici 4))
Tactic:
exact d.mono interior_subset
State after:
no goals

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 ∈ interior (Ici 4), deriv (fun x => 1 / x - k / x ^ p) x ≤ 0
Tactic:
intro x x4
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 : x ∈ interior (Ici 4)
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0

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 : x ∈ interior (Ici 4)
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0
Tactic:
simp only [nonempty_Iio, interior_Ici', mem_Ioi] at x4
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
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0

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
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0
Tactic:
have x0 : 0 < x := by linarith
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
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0

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
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0
Tactic:
simp only [(hd x x4.le).deriv]
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
⊢ -(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2) ≤ 0

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
⊢ -(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2) ≤ 0
Tactic:
simp only [←Real.rpow_mul x0.le, Nat.cast_ofNat, neg_div, mul_div_assoc p, ←
  Real.rpow_sub x0, mul_neg, ←mul_assoc k p, sub_neg_eq_add, neg_add_le_iff_le_add, add_zero,
  ←Real.rpow_two, ←Real.rpow_neg x0.le]
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
⊢ k * p * x ^ (p - 1 - p * 2) ≤ x ^ (-2)

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
⊢ k * p * x ^ (p - 1 - p * 2) ≤ x ^ (-2)
Tactic:
ring_nf
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
⊢ k * p * x ^ (-1 - p) ≤ x ^ (-2)

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
⊢ k * p * x ^ (-1 - p) ≤ x ^ (-2)
Tactic:
simp only [←neg_add', Real.rpow_neg x0.le (1 + p)]
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
⊢ k * p * (x ^ (1 + p))⁻¹ ≤ x ^ (-2)

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
⊢ k * p * (x ^ (1 + p))⁻¹ ≤ x ^ (-2)
Tactic:
rw [mul_inv_le_iff (by positivity), ←Real.rpow_add x0, (by ring_nf : 1 + p + -2 = p - 1)]
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
⊢ k * p ≤ x ^ (p - 1)

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
⊢ k * p ≤ x ^ (p - 1)
Tactic:
have p1' : 1/2 ≤ p - 1 := by linarith
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
⊢ k * p ≤ x ^ (p - 1)

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
⊢ k * p ≤ x ^ (p - 1)
Tactic:
refine le_trans kp (le_trans ?_ (Real.rpow_le_rpow_of_exponent_le (by linarith) p1'))
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
⊢ 2 ≤ x ^ (1 / 2)

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 ≤ x ^ (1 / 2)
Tactic:
rw [one_div, Real.le_rpow_inv_iff_of_pos (by norm_num) x0.le (by norm_num)]
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
⊢ 2 ^ 2 ≤ x

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

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

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

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

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

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

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

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

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