Theorem: LSeriesSummable.mul_bounded (EulerProducts/DirichletLSeries.lean)

State before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
⊢ LSeriesSummable (f * g) s
Tactic:
refine Summable.of_norm <| (hs.const_smul c).norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) fun n ↦ ?_
State after:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖LSeries.term (f * g) s n‖ ≤ ‖c • LSeries.term f s n‖

State before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖LSeries.term (f * g) s n‖ ≤ ‖c • LSeries.term f s n‖
Tactic:
rw [Complex.real_smul, ← LSeries.term_smul_apply, mul_comm]
State after:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖LSeries.term (g * f) s n‖ ≤ ‖LSeries.term (↑c • f) s n‖

State before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖LSeries.term (g * f) s n‖ ≤ ‖LSeries.term (↑c • f) s n‖
Tactic:
refine LSeries.norm_term_le s ?_
State after:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖(g * f) n‖ ≤ ‖(↑c • f) n‖

State before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖(g * f) n‖ ≤ ‖(↑c • f) n‖
Tactic:
have hc : ‖(c : ℂ)‖ = c := by
  simp only [Complex.norm_eq_abs, Complex.abs_ofReal, abs_eq_self, (norm_nonneg _).trans (hg 0)]
State after:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
hc : ‖↑c‖ = c
⊢ ‖(g * f) n‖ ≤ ‖(↑c • f) n‖

State before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
hc : ‖↑c‖ = c
⊢ ‖(g * f) n‖ ≤ ‖(↑c • f) n‖
Tactic:
simpa only [Pi.mul_apply, norm_mul, Pi.smul_apply, smul_eq_mul, hc]
  using mul_le_mul_of_nonneg_right (hg n) <| norm_nonneg _
State after:
no goals

State before:
f g : ℕ → ℂ
c : ℝ
s : ℂ
hs : LSeriesSummable f s
hg : ∀ (n : ℕ), ‖g n‖ ≤ c
n : ℕ
⊢ ‖↑c‖ = c
Tactic:
simp only [Complex.norm_eq_abs, Complex.abs_ofReal, abs_eq_self, (norm_nonneg _).trans (hg 0)]
State after:
no goals