-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem LSeries_eq_mul_integral_aux {f : ℕ → ℂ} (hf : f 0 = 0) {r : ℝ} (hr : 0 ≤ r) {s : ℂ}
    (hs : r < s.re) (hS : LSeriesSummable f s)
    (hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ (n : ℝ) ^ r) :
    LSeries f s = s * ∫ t in Set.Ioi (1 : ℝ), (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (- (s + 1))

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

Tactic:
rwa [sub_pos]

Result:
no goals

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

Tactic:
rw [← Nat.Icc_insert_succ_left n.zero_le, sum_insert (by aesop), hf, zero_add, zero_add]

Result:
no goals

Proof state:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n => ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n => ↑n ^ r
⊢ Tendsto (fun n => ∑ i ∈ range (n + 1), LSeries.term f s i) atTop
    (𝓝 (∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1)))))

Tactic:
simp_rw [Nat.range_succ_eq_Icc_zero, LSeries.term_def₀ hf, mul_comm (f _)]

Result:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n => ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n => ↑n ^ r
⊢ Tendsto (fun n => ∑ x ∈ Icc 0 n, ↑x ^ (-s) * f x) atTop
    (𝓝 (∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1)))))

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

Tactic:
aesop

Result:
no goals

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

Tactic:
simp_rw [← h₄] at hO

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

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

Tactic:
exact isBigO_norm_left.mp <| (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.natCast_atTop

Result:
no goals

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

Tactic:
refine .mul_atTop_rpow_of_isBigO_rpow (-(s + 1).re) r _ ?_ ?_ (by rw [← neg_re, neg_add'])

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

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

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

Tactic:
rw [← neg_re, neg_add']

Result:
no goals

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

Tactic:
refine (integrableOn_Ici_iff_integrableOn_Ioi.mpr <|
  integrableOn_Ioi_deriv_ofReal_cpow zero_lt_one
    (by simpa using hr.trans_lt hs)).locallyIntegrableOn

Result:
no goals

Proof state:
case h.e'_5.h.e'_3
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n => ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n => ↑n ^ r
⊢ ∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1))) =
    0 - ∫ (t : ℝ) in Set.Ioi 1, deriv (fun x => ↑x ^ (-s)) t * ∑ k ∈ Icc 0 ⌊t⌋₊, f k

Tactic:
rw [zero_sub, ← integral_neg]

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

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

Tactic:
rwa [sub_re, one_re, neg_re, neg_sub_left, neg_add_lt_iff_lt_add, add_neg_cancel_comm]

Result:
no goals

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

Tactic:
simpa using hr.trans_lt hs

Result:
no goals