-- Mathlib/NumberTheory/LSeries/Basic.lean
/-- If `f n` is bounded in absolute value by a constant times `n^(x-1)` and `re s > x`,
then the `LSeries` of `f` is summable at `s`. -/
lemma LSeriesSummable_of_le_const_mul_rpow {f : ℕ → ℂ} {x : ℝ} {s : ℂ} (hs : x < s.re)
    (h : ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C * n ^ (x - 1)) :
    LSeriesSummable f s

Proof state:
case intro
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
⊢ LSeriesSummable f s

Tactic:
refine Summable.of_norm <| hsum.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ ?_)

Result:
case intro
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
⊢ ‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖

Proof state:
case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
n : ℕ
hn : n ≥ 1
⊢ ‖↑n ^ (-(s + (1 - ↑x)))‖ = ↑n ^ (-s.re + x - 1)

Tactic:
simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]

Result:
case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
n : ℕ
hn : n ≥ 1
⊢ ↑n ^ (-(s.re + (1 - x))) = ↑n ^ (-s.re + x - 1)

Proof state:
case intro.inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
⊢ ‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖

Tactic:
have hn' : 0 < (n : ℝ) ^ s.re := Real.rpow_pos_of_pos (Nat.cast_pos.mpr hn) _

Result:
case intro.inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
hn' : 0 < ↑n ^ s.re
⊢ ‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖

Proof state:
case intro
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
⊢ LSeriesSummable f s

Tactic:
have hC₀ : 0 ≤ C := (norm_nonneg <| f 1).trans <| by simpa using hC 1 one_ne_zero

Result:
case intro
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
⊢ LSeriesSummable f s

Proof state:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ Summable fun n => ‖↑C‖ * ‖↑n ^ (-(s + (1 - ↑x)))‖

Tactic:
refine Summable.mul_left _ <|
  Summable.of_norm_bounded_eventually_nat (fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_

Result:
case refine_1
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ Summable fun n => ↑n ^ (-s.re + x - 1)

case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ ∀ᶠ (i : ℕ) in Filter.atTop, ‖‖↑i ^ (-(s + (1 - ↑x)))‖‖ ≤ (fun n => ↑n ^ (-s.re + x - 1)) i

Proof state:
case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
n : ℕ
hn : n ≥ 1
⊢ ↑n ^ (-(s.re + (1 - x))) = ↑n ^ (-s.re + x - 1)

Tactic:
ring_nf

Result:
no goals

Proof state:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
⊢ Summable fun n => ‖↑C‖ * ‖↑n ^ (-(s + (1 - ↑x)))‖

Tactic:
have hsx : -s.re + x - 1 < -1 := by linarith only [hs]

Result:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ Summable fun n => ‖↑C‖ * ‖↑n ^ (-(s + (1 - ↑x)))‖

Proof state:
case intro
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
⊢ ‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Result:
case intro.inl
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
⊢ ‖term f s 0‖ ≤ ‖↑C / ↑0 ^ (s + (1 - ↑x))‖

case intro.inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
⊢ ‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖

Proof state:
case intro.inl
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
⊢ ‖term f s 0‖ ≤ ‖↑C / ↑0 ^ (s + (1 - ↑x))‖

Tactic:
simpa only [term_zero, norm_zero] using norm_nonneg _

Result:
no goals

Proof state:
case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ ∀ᶠ (i : ℕ) in Filter.atTop, ‖‖↑i ^ (-(s + (1 - ↑x)))‖‖ ≤ (fun n => ↑n ^ (-s.re + x - 1)) i

Tactic:
simp only [norm_norm, Filter.eventually_atTop]

Result:
case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ ∃ a, ∀ b ≥ a, ‖↑b ^ (-(s + (1 - ↑x)))‖ ≤ ↑b ^ (-s.re + x - 1)

Proof state:
case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ ∃ a, ∀ b ≥ a, ‖↑b ^ (-(s + (1 - ↑x)))‖ ≤ ↑b ^ (-s.re + x - 1)

Tactic:
refine ⟨1, fun n hn ↦ le_of_eq ?_⟩

Result:
case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
n : ℕ
hn : n ≥ 1
⊢ ‖↑n ^ (-(s + (1 - ↑x)))‖ = ↑n ^ (-s.re + x - 1)

Proof state:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
⊢ LSeriesSummable f s

Tactic:
obtain ⟨C, hC⟩ := h

Result:
case intro
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
⊢ LSeriesSummable f s

Proof state:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
⊢ ‖f 1‖ ≤ C

Tactic:
simpa using hC 1 one_ne_zero

Result:
no goals

Proof state:
case intro.inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
hn' : 0 < ↑n ^ s.re
⊢ ‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖

Tactic:
simp_rw [term_of_ne_zero hn.ne', norm_div, norm_natCast_cpow_of_pos hn, div_le_iff₀ hn',
  norm_real, Real.norm_of_nonneg hC₀, div_eq_mul_inv, mul_assoc,
  ← Real.rpow_neg <| Nat.cast_nonneg _, ← Real.rpow_add <| Nat.cast_pos.mpr hn]

Result:
case intro.inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
hn' : 0 < ↑n ^ s.re
⊢ ‖f n‖ ≤ C * ↑n ^ (-(s + (1 - ↑x)).re + s.re)

Proof state:
case refine_1
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ Summable fun n => ↑n ^ (-s.re + x - 1)

Tactic:
simpa

Result:
no goals

Proof state:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
⊢ -s.re + x - 1 < -1

Tactic:
linarith only [hs]

Result:
no goals

Proof state:
case intro.inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
hn' : 0 < ↑n ^ s.re
⊢ ‖f n‖ ≤ C * ↑n ^ (-(s + (1 - ↑x)).re + s.re)

Tactic:
simpa using hC n <| Nat.pos_iff_ne_zero.mp hn

Result:
no goals