English
The abscissa of absolute convergence of logMul f equals that of f.
Русский
Абсцисса абсолютной сходимости logMul f равна абсциссе f.
LaTeX
$$abscissaOfAbsConv (logMul f) = abscissaOfAbsConv f$$
Lean4
/-- The abscissa of absolute convergence of the point-wise product of `log` and `f`
is the same as that of `f`. -/
@[simp]
theorem abscissaOfAbsConv_logMul {f : ℕ → ℂ} : abscissaOfAbsConv (logMul f) = abscissaOfAbsConv f :=
by
apply le_antisymm <;> refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun s hs ↦ ?_
· exact LSeriesSummable_logMul_of_lt_re <| by simp [hs]
· refine
(LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simp [hs]) |>.norm.of_norm_bounded_eventually_nat (g := fun n ↦
‖term (logMul f) s n‖) ?_
filter_upwards [Filter.eventually_ge_atTop <| max 1 (Nat.ceil (Real.exp 1))] with n hn
simp only [term_of_ne_zero (show n ≠ 0 by omega), logMul, norm_mul, mul_div_assoc, ← natCast_log, norm_real]
refine le_mul_of_one_le_left (norm_nonneg _) (.trans ?_ <| Real.le_norm_self _)
simpa using Real.log_le_log (Real.exp_pos 1) <| Nat.ceil_le.mp <| (le_max_right _ _).trans hn
