-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
/-- Power asymptotic for `f - f₀` as `x → 0`. -/
lemma hf_zero' (P : WeakFEPair E) :
    (fun x : ℝ ↦ P.f x - P.f₀) =O[𝓝[>] 0] (· ^ (-P.k))

Proof state:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => ‖(P.ε * ↑(x ^ (-P.k))) • P.g₀‖) =O[𝓝[>] 0] fun x => ‖x ^ (-P.k)‖

Tactic:
simp_rw [mul_smul, norm_smul, mul_comm _ ‖P.g₀‖, ← mul_assoc, norm_real]

Result:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => ‖P.ε‖ * ‖P.g₀‖ * ‖x ^ (-P.k)‖) =O[𝓝[>] 0] fun x => ‖x ^ (-P.k)‖

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖

Tactic:
apply le_mul_of_one_le_right (norm_nonneg _)

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ 1 ≤ ‖x ^ (-P.k)‖

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => P.f₀) =O[𝓝[>] 0] fun x => x ^ (-P.k)

Tactic:
refine IsBigO.of_bound ‖P.f₀‖ (eventually_nhdsWithin_iff.mpr ?_)

Result:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ 1 ≤ ‖x ^ (-P.k)‖

Tactic:
rw [norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_neg hx.le]

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ 1 ≤ (x ^ P.k)⁻¹

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖

Tactic:
filter_upwards [eventually_le_nhds zero_lt_one] with x hx' (hx : 0 < x)

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖

Proof state:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => ‖P.ε‖ * ‖P.g₀‖ * ‖x ^ (-P.k)‖) =O[𝓝[>] 0] fun x => ‖x ^ (-P.k)‖

Tactic:
apply (isBigO_refl _ _).const_mul_left

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => P.f x - P.f₀) =O[𝓝[>] 0] fun x => x ^ (-P.k)

Tactic:
simp_rw [← fun x ↦ sub_add_sub_cancel (P.f x) ((P.ε * ↑(x ^ (-P.k))) • P.g₀) P.f₀]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀ + ((P.ε * ↑(x ^ (-P.k))) • P.g₀ - P.f₀)) =O[𝓝[>] 0] fun x => x ^ (-P.k)

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ 1 ≤ (x ^ P.k)⁻¹

Tactic:
exact (one_le_inv₀ (rpow_pos_of_pos hx _)).2 (rpow_le_one hx.le hx' P.hk.le)

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀ + ((P.ε * ↑(x ^ (-P.k))) • P.g₀ - P.f₀)) =O[𝓝[>] 0] fun x => x ^ (-P.k)

Tactic:
refine (P.hf_zero _).add (IsBigO.sub ?_ ?_)

Result:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x => x ^ (-P.k)

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => P.f₀) =O[𝓝[>] 0] fun x => x ^ (-P.k)

Proof state:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x => x ^ (-P.k)

Tactic:
rw [← isBigO_norm_norm]

Result:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x => ‖(P.ε * ↑(x ^ (-P.k))) • P.g₀‖) =O[𝓝[>] 0] fun x => ‖x ^ (-P.k)‖