-- Mathlib/Analysis/MellinTransform.lean
theorem isBigO_rpow_zero_log_smul [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (hab : a < b)
    (hf : f =O[𝓝[>] 0] (· ^ (-a))) :
    (fun t : ℝ => log t • f t) =O[𝓝[>] 0] (· ^ (-b))

Proof state:
case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
this : log =o[𝓝[>] 0] fun t => t ^ (a - b)
t : ℝ
ht : t ∈ Ioi 0
⊢ a - b + -a = -b

Tactic:
abel

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
this : log =o[𝓝[>] 0] fun t => t ^ (a - b)
t : ℝ
⊢ (fun x => log x • f x) t = (fun t => log t • f t) t

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
this : log =o[𝓝[>] 0] fun t => t ^ (a - b)
⊢ (fun t => log t • f t) =O[𝓝[>] 0] fun x => x ^ (-b)

Tactic:
refine (this.isBigO.smul hf).congr' (Eventually.of_forall fun t => by rfl)
    (eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ?_))

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
this : log =o[𝓝[>] 0] fun t => t ^ (a - b)
t : ℝ
ht : t ∈ Ioi 0
⊢ (fun x => x ^ (a - b) • x ^ (-a)) t = (fun x => x ^ (-b)) t

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
this : log =o[𝓝[>] 0] fun t => t ^ (a - b)
t : ℝ
ht : t ∈ Ioi 0
⊢ (fun x => x ^ (a - b) • x ^ (-a)) t = (fun x => x ^ (-b)) t

Tactic:
simp_rw [smul_eq_mul, ← rpow_add ht]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
this : log =o[𝓝[>] 0] fun t => t ^ (a - b)
t : ℝ
ht : t ∈ Ioi 0
⊢ t ^ (a - b + -a) = t ^ (-b)

Proof state:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
t : ℝ
⊢ ((fun x => -log x) ∘ fun x => x⁻¹) t = log t

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
this : log =o[𝓝[>] 0] fun t => t ^ (a - b)
t : ℝ
ht : t ∈ Ioi 0
⊢ t ^ (a - b + -a) = t ^ (-b)

Tactic:
congr 1

Result:
case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
this : log =o[𝓝[>] 0] fun t => t ^ (a - b)
t : ℝ
ht : t ∈ Ioi 0
⊢ a - b + -a = -b

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
⊢ log =o[𝓝[>] 0] fun t => t ^ (a - b)

Tactic:
refine ((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).neg_left.comp_tendsto
      tendsto_inv_nhdsGT_zero).congr'
  (.of_forall fun t => ?_)
  (eventually_mem_nhdsWithin.mono fun t ht => ?_)

Result:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
t : ℝ
⊢ ((fun x => -log x) ∘ fun x => x⁻¹) t = log t

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
t : ℝ
ht : t ∈ Ioi 0
⊢ ((fun x => x ^ (b - a)) ∘ fun x => x⁻¹) t = (fun t => t ^ (a - b)) t

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x => x ^ (-a)
t : ℝ
ht : t ∈ Ioi 0
⊢ ((fun x => x ^ (b - a)) ∘ fun x => x⁻¹) t = (fun t => t ^ (a - b)) t

Tactic:
simp_rw [Function.comp_apply, inv_rpow (le_of_lt ht), ← rpow_neg (le_of_lt ht), neg_sub]

Result:
no goals