apply (isLittleO_log_rpow_atTop (by linarith) ..).isBigO
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x.log) =O[atTop] fun x => x ^ ((1 - r) / 2)

case h₀
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ᶠ (x : ℝ) in atTop, x.log = 0 → x ^ ((1 - r) / 2) = 0
case h₀
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ᶠ (x : ℝ) in atTop, x.log = 0 → x ^ ((1 - r) / 2) = 0