-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem LSeriesSummable_of_sum_norm_bigO_aux (hf : f 0 = 0)
    (hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ (n : ℝ) ^ r)
    (hr : 0 ≤ r) (hs : r < s.re) :
    LSeriesSummable f s

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))
⊢ Summable fun x => ↑x ^ (-s) * f x

Tactic:
refine summable_mul_of_bigO_atTop' (f := fun t ↦ (t : ℂ) ^ (-s))
  (g := fun t ↦ t ^ (-(s.re + 1) + r)) _ h₃ ?_ ?_ ?_ ?_

Result:
case refine_1
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))
⊢ LocallyIntegrableOn (deriv fun t => ‖(fun t => ↑t ^ (-s)) t‖) (Set.Ici 1) volume

case refine_2
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))
⊢ (fun n => ‖(fun t => ↑t ^ (-s)) ↑n‖ * ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun x => 1

case refine_3
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))
⊢ (fun t => deriv (fun t => ‖(fun t => ↑t ^ (-s)) t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) =O[atTop] fun t =>
    t ^ (-(s.re + 1) + r)

case refine_4
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))
⊢ IntegrableAtFilter (fun t => t ^ (-(s.re + 1) + r)) atTop volume

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))
⊢ ∀ (x : ℕ), ↑x ^ 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
⊢ (-s).re + r ≤ 0

Tactic:
rw [neg_re, neg_add_nonpos_iff]

Result:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
⊢ r ≤ s.re

Proof state:
case refine_2
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))
⊢ (fun n => ‖(fun t => ↑t ^ (-s)) ↑n‖ * ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun x => 1

Tactic:
refine (IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow _ _ _ ?_ hO h₂).congr_right  (by simp)

Result:
case refine_2
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))
⊢ (fun n => ‖(fun t => ↑t ^ (-s)) ↑n‖) =O[atTop] fun n => ↑n ^ (-s).re

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))
⊢ LSeriesSummable f s

Tactic:
simp_rw [LSeriesSummable, funext (LSeries.term_def₀ hf s), mul_comm (f _)]

Result:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))
⊢ Summable fun x => ↑x ^ (-s) * f x

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
⊢ (deriv fun t => ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t => -s.re * t ^ (-(s.re + 1))

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Result:
case h
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
t : ℝ
ht : 0 < t
⊢ deriv (fun t => ‖↑t ^ (-s)‖) t = -s.re * t ^ (-(s.re + 1))

Proof state:
case h
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖↑x ^ (-s)‖) t
t : ℝ
ht : 0 < t
⊢ deriv (fun t => ‖↑t ^ (-s)‖) t = -s.re * t ^ (-(s.re + 1))

Tactic:
rw [deriv_norm_ofReal_cpow _ ht, neg_re, neg_add']

Result:
no goals