-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem lemma₂ {s T ε : ℝ} {S : ℝ → ℂ} (hs : 1 < s)
    (hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1)) (hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t) :
    IntegrableOn (fun t : ℝ ↦ ‖S t‖ * (t ^ (-s - 1))) (Set.Ici 1)

Proof state:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ ContinuousOn (fun t => t ^ (-s - 1)) (Set.Ici 1)

Tactic:
exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
  <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt

Result:
no goals

Proof state:
case refine_1
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ ∀ᶠ (x : ℝ) in atTop, ‖‖S x‖ * x ^ (-s - 1)‖ ≤ ε * ‖x ^ (-s)‖

Tactic:
filter_upwards [eventually_ge_atTop T, eventually_gt_atTop 0] with t ht ht'

Result:
case h
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
t : ℝ
ht : T ≤ t
ht' : 0 < t
⊢ ‖‖S t‖ * t ^ (-s - 1)‖ ≤ ε * ‖t ^ (-s)‖

Proof state:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ LocallyIntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
refine hS₁.norm.mul_continuousOn ?_ isLocallyClosed_Ici

Result:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ ContinuousOn (fun t => t ^ (-s - 1)) (Set.Ici 1)

Proof state:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ IntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
refine h.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^(-s)) (isBigO_iff.mpr ⟨ε, ?_⟩) ?_

Result:
case refine_1
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ ∀ᶠ (x : ℝ) in atTop, ‖‖S x‖ * x ^ (-s - 1)‖ ≤ ε * ‖x ^ (-s)‖

case refine_2
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ IntegrableAtFilter (fun t => t ^ (-s)) atTop volume

Proof state:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ IntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
have h : LocallyIntegrableOn (fun t : ℝ ↦ ‖S t‖ * (t ^ (-s - 1))) (Set.Ici 1) := by
  refine hS₁.norm.mul_continuousOn ?_ isLocallyClosed_Ici
  exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
    <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt

Result:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ IntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Proof state:
case refine_2
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ IntegrableAtFilter (fun t => t ^ (-s)) atTop volume

Tactic:
exact integrableAtFilter_rpow_atTop_iff.mpr <| neg_lt_neg_iff.mpr hs

Result:
no goals

Proof state:
case h
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t => S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
t : ℝ
ht : T ≤ t
ht' : 0 < t
⊢ ‖‖S t‖ * t ^ (-s - 1)‖ ≤ ε * ‖t ^ (-s)‖

Tactic:
simpa [abs_of_nonneg, Real.rpow_nonneg, ht'.le, Real.rpow_sub ht', mul_assoc, ht'.ne',
  mul_div_cancel₀] using mul_le_mul_of_nonneg_right (hS₂ t ht) (norm_nonneg <| t ^ (-s - 1))

Result:
no goals