ArithmeticFunction.LSeriesSummable.of_norm_le_norm

@[blueprint  "LSeriesSummable_two_pow_omega"  (title := "LSeriesSummable-two-pow-omega")  (statement := /--    An L-series is convergent if the absolute value of each term is term wise less than a summable series.  -/)  (proof := /--    Apply triangle inequality and comparison test.  -/)]lemma LSeriesSummable.of_norm_le_norm {f g : ℕ → ℂ} {s : ℂ}  (hgf : ∀ (n : ℕ), ‖LSeries.term (fun n ↦ g n) s n‖ ≤ ‖LSeries.term (fun n ↦ f n) s n‖)  (hf : Summable (fun n ↦ ‖LSeries.term (fun n ↦ f n) s n‖)) : LSeriesSummable (fun n ↦ g n) s := by  have h_fSummable : LSeriesSummable (fun n => f n) s := by    rw [LSeriesSummable, ← summable_norm_iff]    exact hf  rw [LSeriesSummable, ← summable_norm_iff] at *  apply Summable.of_nonneg_of_le (fun n => norm_nonneg _) (fun n => _) h_fSummable  exact hgf