abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable

English

If for every y > x the L-series L(f,y) converges, then abscissaOfAbsConv f ≤ x.

Русский

Если для каждого y > x серия сходится, то abscissaOfAbsConv f ≤ x.

LaTeX

$$$\\forall x\\in\\mathbb{R},\\; (\\forall y> x,\\ LSeriesSummable\\ f\\ y)\\Rightarrow \\operatorname{abscissaOfAbsConv}(f) \\le x.$$$

Lean4

theorem abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable {f : ℕ → ℂ} {x : ℝ}
    (h : ∀ y : ℝ, x < y → LSeriesSummable f y) : abscissaOfAbsConv f ≤ x :=
  by
  refine sInf_le_iff.mpr fun y hy ↦ le_of_forall_gt_imp_ge_of_dense fun a ↦ ?_
  replace hy : ∀ (a : ℝ), LSeriesSummable f a → y ≤ a := by simpa [mem_lowerBounds] using hy
  cases a with
  | coe a₀ => exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)
  | bot => simp
  | top => simp

Похожие утверждения