-- 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
⊢ LSeriesSummable f s

Tactic:
have h₃ (t : ℝ) (ht : t ∈ Set.Ici 1) : DifferentiableAt ℝ (fun x : ℝ ↦ ‖(x : ℂ) ^ (-s)‖) t :=
  have ht' : t ≠ 0 := (zero_lt_one.trans_le ht).ne'
  (differentiableAt_id.ofReal_cpow_const ht' h₁).norm ℝ <|
    (cpow_ne_zero_iff_of_exponent_ne_zero h₁).mpr <| ofReal_ne_zero.mpr ht'

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
⊢ 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
⊢ LSeriesSummable f s

Tactic:
have h₄ : (deriv fun t : ℝ ↦ ‖(t : ℂ) ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re +1)) := by
  filter_upwards [eventually_gt_atTop 0] with t ht
  rw [deriv_norm_ofReal_cpow _ ht, neg_re, neg_add']

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))
⊢ LSeriesSummable f s

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‖) =O[atTop] fun n => ↑n ^ (-s).re

Tactic:
exact (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.natCast_atTop

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
⊢ LSeriesSummable f s

Tactic:
have h₂ : (-s).re + r ≤ 0 := by
  rw [neg_re, neg_add_nonpos_iff]
  exact hs.le

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
⊢ LSeriesSummable f s

Proof state:
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 => ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) =O[atTop] fun t => t ^ r

Tactic:
exact (hO.comp_tendsto tendsto_nat_floor_atTop).trans <|
  isEquivalent_nat_floor.isBigO.rpow hr (eventually_ge_atTop 0)

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
⊢ LSeriesSummable f s

Tactic:
have h₁ : -s ≠ 0 := neg_ne_zero.mpr <| ne_zero_of_re_pos (hr.trans_lt hs)

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
⊢ LSeriesSummable f s

Proof state:
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

Tactic:
rwa [integrableAtFilter_rpow_atTop_iff, neg_add_lt_iff_lt_add, add_neg_cancel_right]

Result:
no goals

Proof state:
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))
⊢ (-s).re ≤ 0

Tactic:
exact neg_re _ ▸ neg_nonpos.mpr  <| hr.trans hs.le

Result:
no goals

Proof state:
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

Tactic:
refine (integrableOn_Ici_iff_integrableOn_Ioi.mpr
  (integrableOn_Ioi_deriv_norm_ofReal_cpow zero_lt_one ?_)).locallyIntegrableOn

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))
⊢ (-s).re ≤ 0

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
⊢ r ≤ s.re

Tactic:
exact hs.le

Result:
no goals

Proof state:
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)

Tactic:
refine h₄.isBigO.of_const_mul_right.mul_atTop_rpow_of_isBigO_rpow _ r _ ?_ le_rfl

Result:
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 => ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) =O[atTop] fun t => t ^ r