-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem lemma₁ (hlim : Tendsto (fun n : ℕ ↦ (∑ k ∈ Icc 1 n, f k) / n) atTop (𝓝 l))
    {s : ℝ} (hs : 1 < s) :
    IntegrableOn (fun t : ℝ ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (t : ℂ) ^ (-(s : ℂ) - 1)) (Set.Ici 1)

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t

Tactic:
refine IsBigO.trans_isEquivalent ?_ isEquivalent_nat_floor

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun x => ↑⌊x⌋₊

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t ^ 1

Tactic:
simp_rw [Real.rpow_one]

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun x => ↑⌊x⌋₊

Tactic:
have : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ((n : ℝ) ^ (1 : ℝ) : ℝ)) atTop (𝓝 l) := by
  simpa using hlim

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
this : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑(↑n ^ 1)) atTop (𝓝 l)
⊢ (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun x => ↑⌊x⌋₊

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (fun t => ↑t ^ (-↑s - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k) (Set.Ici 1) volume

Tactic:
refine locallyIntegrableOn_mul_sum_Icc f zero_le_one ?_

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (fun t => ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (fun t => ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Tactic:
refine ContinuousOn.locallyIntegrableOn (fun t ht ↦ ?_) measurableSet_Ici

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
t : ℝ
ht : t ∈ Set.Ici 1
⊢ ContinuousWithinAt (fun t => ↑t ^ (-↑s - 1)) (Set.Ici 1) t

Proof state:
case refine_1
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t ^ 1
⊢ (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) =O[atTop] fun t => t ^ (-s)

Tactic:
refine IsBigO.mul_atTop_rpow_of_isBigO_rpow 1 (-s - 1) _ h₂ ?_ (by linarith)

Result:
case refine_1
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t ^ 1
⊢ (fun t => ↑t ^ (-↑s - 1)) =O[atTop] fun t => t ^ (-s - 1)

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Tactic:
simp_rw [mul_comm]

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (fun t => ↑t ^ (-↑s - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k) (Set.Ici 1) volume

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t ^ 1
⊢ IntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Tactic:
refine h₁.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^(-s)) ?_ ?_

Result:
case refine_1
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t ^ 1
⊢ (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) =O[atTop] fun t => t ^ (-s)

case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t ^ 1
⊢ IntegrableAtFilter (fun t => t ^ (-s)) atTop volume

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
t : ℝ
ht : t ∈ Set.Ici 1
⊢ ContinuousWithinAt (fun t => ↑t ^ (-↑s - 1)) (Set.Ici 1) t

Tactic:
exact (continuousAt_ofReal_cpow_const _ _ <|
  Or.inr (zero_lt_one.trans_le ht).ne').continuousWithinAt

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ IntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Tactic:
have h₂ : (fun t : ℝ ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ (1 : ℝ) := by
  simp_rw [Real.rpow_one]
  refine IsBigO.trans_isEquivalent ?_ isEquivalent_nat_floor
  have : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ((n : ℝ) ^ (1 : ℝ) : ℝ)) atTop (𝓝 l) := by
    simpa using hlim
  simpa using (isBigO_atTop_natCast_rpow_of_tendsto_div_rpow this).comp_tendsto
      tendsto_nat_floor_atTop

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t ^ 1
⊢ IntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Proof state:
case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t ^ 1
⊢ IntegrableAtFilter (fun t => t ^ (-s)) atTop volume

Tactic:
rwa [integrableAtFilter_rpow_atTop_iff, neg_lt_neg_iff]

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t ^ 1
⊢ 1 + (-s - 1) ≤ -s

Tactic:
linarith

Result:
no goals