internlm/Lean-Github huggingface dataset:
Theorem: pass_through
Proof state before:
case right
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
fs : Complex.abs (f' 2 c ((f' 2 c)^[k - 1] z)) ≤ Complex.abs ((f' 2 c)^[k - 1] z) ^ 2 + Complex.abs c
⊢ Complex.abs ((f' 2 c)^[k] z) ≤ 20
Tactic:
simp only [←Function.iterate_succ_apply', Nat.succ_eq_add_one, Nat.sub_add_cancel k1] at fs
Proof state after:
case right
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
fs : Complex.abs ((f' 2 c)^[k] z) ≤ Complex.abs ((f' 2 c)^[k - 1] z) ^ 2 + Complex.abs c
⊢ Complex.abs ((f' 2 c)^[k] z) ≤ 20
Theorem: pass_through
Proof state before:
case right
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
fs : Complex.abs ((f' 2 c)^[k] z) ≤ Complex.abs ((f' 2 c)^[k - 1] z) ^ 2 + Complex.abs c
⊢ Complex.abs ((f' 2 c)^[k] z) ≤ 20
Tactic:
exact le_trans fs (le_trans (add_le_add (pow_le_pow_left (Complex.abs.nonneg _) lt 2) c4)
  (by norm_num))
Proof state after:
no goals
Theorem: pass_through
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
⊢ p n
Tactic:
rw [←hp]
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
⊢ (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) n
Theorem: pass_through
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
⊢ (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) n
Tactic:
linarith [h n (by linarith)]
Proof state after:
no goals
Theorem: pass_through
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
⊢ n ≤ n
Tactic:
linarith
Proof state after:
no goals
Theorem: pass_through
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
⊢ p k
Tactic:
rw [←hk]
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
⊢ p (Nat.find ⋯)
Theorem: pass_through
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
⊢ p (Nat.find ⋯)
Tactic:
exact Nat.find_spec (p := p) ⟨_,h⟩
Proof state after:
no goals
Theorem: pass_through
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
⊢ k ≠ 0
Tactic:
contrapose k4
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : ¬k ≠ 0
⊢ ¬p k
Theorem: pass_through
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : ¬k ≠ 0
⊢ ¬p k
Tactic:
simp only [not_not] at k4
Proof state after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : k = 0
⊢ ¬p k
Theorem: pass_through
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : k = 0
⊢ ¬p k
Tactic:
simp only [k4, ←hp, not_lt, Function.iterate_zero_apply, z4]
Proof state after:
no goals
Theorem: pass_through
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ ¬p (k - 1)
Tactic:
apply Nat.find_min
Proof state after:
case a
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ k - 1 < Nat.find ?H

case H
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ ∃ n, p n
Theorem: pass_through
Proof state before:
case a
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ k - 1 < Nat.find ?H

case H
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ ∃ n, p n
Tactic:
rw [hk]
Proof state after:
case a
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ k - 1 < k
Theorem: pass_through
Proof state before:
case a
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ k - 1 < k
Tactic:
omega
Proof state after:
no goals
Theorem: pass_through
Proof state before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
fs : Complex.abs ((f' 2 c)^[k] z) ≤ Complex.abs ((f' 2 c)^[k - 1] z) ^ 2 + Complex.abs c
⊢ 4 ^ 2 + 4 ≤ 20
Tactic:
norm_num
Proof state after:
no goals
Theorem: lower_anti
Proof 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)
Proof 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)
Theorem: lower_anti
Proof 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
Proof 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)
Theorem: lower_anti
Proof state before:
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
⊢ 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
Proof 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)
Theorem: lower_anti
Proof state before:
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
⊢ AntitoneOn (fun x => 1 / x - k / x ^ p) (Ici 4)
Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ici _)
Proof 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
Theorem: lower_anti
Proof 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
Proof 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
Theorem: lower_anti
Proof 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]
Proof 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
Theorem: lower_anti
Proof 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 _ ?_)
Proof 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
Theorem: lower_anti
Proof 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)
Proof state after:
no goals
Theorem: lower_anti
Proof 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
Proof state after:
no goals
Theorem: lower_anti
Proof 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
Proof state after:
no goals
Theorem: lower_anti
Proof 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
Proof state after:
no goals
Theorem: lower_anti
Proof 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
Proof state after:
no goals
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
⊢ ∀ x ∈ interior (Ici 4), deriv (fun x => 1 / x - k / x ^ p) x ≤ 0
Tactic:
intro x x4
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : x ∈ interior (Ici 4)
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 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
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0
Tactic:
have x0 : 0 < x := by linarith
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ deriv (fun x => 1 / x - k / x ^ p) x ≤ 0
Tactic:
simp only [(hd x x4.le).deriv]
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ -(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2) ≤ 0
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ -(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]
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ k * p * x ^ (p - 1 - p * 2) ≤ x ^ (-2)
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ k * p * x ^ (p - 1 - p * 2) ≤ x ^ (-2)
Tactic:
ring_nf
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ k * p * x ^ (-1 - p) ≤ x ^ (-2)
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ k * p * x ^ (-1 - p) ≤ x ^ (-2)
Tactic:
simp only [←neg_add', Real.rpow_neg x0.le (1 + p)]
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ k * p * (x ^ (1 + p))⁻¹ ≤ x ^ (-2)
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ 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)]
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ k * p ≤ x ^ (p - 1)
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
⊢ k * p ≤ x ^ (p - 1)
Tactic:
have p1' : 1/2 ≤ p - 1 := by linarith
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ k * p ≤ x ^ (p - 1)
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ k * p ≤ x ^ (p - 1)
Tactic:
refine le_trans kp (le_trans ?_ (Real.rpow_le_rpow_of_exponent_le (by linarith) p1'))
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ 2 ≤ x ^ (1 / 2)
Theorem: lower_anti
Proof state before:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ 2 ≤ x ^ (1 / 2)
Tactic:
rw [one_div, Real.le_rpow_inv_iff_of_pos (by norm_num) x0.le (by norm_num)]
Proof state after:
case hf'_nonpos
c z : ℂ
k p : ℝ
hd : ∀ (x : ℝ), 4 ≤ x → HasDerivAt (fun x => 1 / x - k / x ^ p) (-(x ^ 2)⁻¹ - k * (-(p * x ^ (p - 1)) / (x ^ p) ^ 2)) x
kp : k * p ≤ 2
hp : 3 / 2 ≤ p
d : DifferentiableOn ℝ (fun x => 1 / x - k / x ^ p) (Ici 4)
x : ℝ
x4 : 4 < x
x0 : 0 < x
p1' : 1 / 2 ≤ p - 1
⊢ 2 ^ 2 ≤ x