-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div
    (hlim : Tendsto (fun n : ℕ ↦ (∑ k ∈ Icc 1 n, f k) / n) atTop (𝓝 l))
    (hfS : ∀ s : ℝ, 1 < s → LSeriesSummable f s) :
    Tendsto (fun s : ℝ ↦ (s - 1) * LSeries f s) (𝓝[>] 1) (𝓝 l)

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
C ε : ℝ
⊢ Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)

Tactic:
rw [show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring]

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
C ε : ℝ
⊢ Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ((1 - 1) * 1 * C + 1 * ε))

Proof state:
case refine_1
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ 0 ≤ liminf (fun x => ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1)

Tactic:
exact le_liminf_of_le h₂.isCoboundedUnder_ge (univ_mem' (fun _ ↦ norm_nonneg _))

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
this : Tendsto (fun s => (↑s - 1) * LSeries f ↑s - ↑s * l) (𝓝[>] 1) (𝓝 0)
h₃ : Tendsto (fun s => ↑s * l) (𝓝[>] 1) (𝓝 (1 * l))
x✝ : ℝ
⊢ (↑x✝ - 1) * LSeries f ↑x✝ - ↑x✝ * l + ↑x✝ * l = (↑x✝ - 1) * LSeries f ↑x✝

Tactic:
ring

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
⊢ Tendsto (fun s => (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Tactic:
have h₁ {C ε : ℝ} : Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε) := by
  rw [show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring]
  exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
⊢ Tendsto (fun s => (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Proof state:
case e_x
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
C ε : ℝ
⊢ ε = (1 - 1) * 1 * C + 1 * ε

Tactic:
ring

Result:
no goals

Proof state:
case refine_3
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (𝓝[>] 1) fun x => ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖

Tactic:
exact isBoundedUnder_of_eventually_ge (univ_mem' fun _ ↦ norm_nonneg _)

Result:
no goals

Proof state:
case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ limsup (fun x => ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ 0

Tactic:
refine le_of_forall_pos_le_add fun ε hε ↦ ?_

Result:
case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
ε : ℝ
hε : 0 < ε
⊢ limsup (fun x => ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ 0 + ε

Proof state:
case refine_2.intro.intro
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
ε : ℝ
hε : 0 < ε
C : ℝ
hC₁ : C ≥ 0
hC₂ : (fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖) ≤ᶠ[𝓝[>] 1] fun s => (s - 1) * s * C + s * ε
⊢ limsup (fun x => ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ ε

Tactic:
refine le_of_le_of_eq (limsup_le_limsup hC₂ ?_ h₁.isBoundedUnder_le) h₁.limsup_eq

Result:
case refine_2.intro.intro
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
ε : ℝ
hε : 0 < ε
C : ℝ
hC₁ : C ≥ 0
hC₂ : (fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖) ≤ᶠ[𝓝[>] 1] fun s => (s - 1) * s * C + s * ε
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun x => ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖

Proof state:
case intro.intro
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
C : ℝ
left✝ : C ≥ 0
hC₂ : (fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖) ≤ᶠ[𝓝[>] 1] fun s => (s - 1) * s * C + s * 1
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖

Tactic:
exact h₁.isBoundedUnder_le.mono_le hC₂

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
⊢ Tendsto (fun s => (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Tactic:
have h₂ : IsBoundedUnder
    (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s : ℝ ↦ ‖(s - 1) * LSeries f s - s * l‖ := by
  obtain ⟨C, _, hC₂⟩ :=
    LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS zero_lt_one
  exact h₁.isBoundedUnder_le.mono_le hC₂

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s => (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ Tendsto (fun s => (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)