abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'

English

If x ∈ EReal and for all real y with x < y we have LSeriesSummable f y, then abscissaOfAbsConv f ≤ x.

Русский

Если x принадлежит расширенным вещественным числам и для каждого действительного y с x < y выполняется LSeriesSummable f y, то abscissaOfAbsConv f ≤ x.

LaTeX

$$$\\forall x\\in\\mathbb{E},\\; (\\forall y\\in\\mathbb{R}, x

Lean4

theorem abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' {f : ℕ → ℂ} {x : EReal}
    (h : ∀ y : ℝ, x < y → LSeriesSummable f y) : abscissaOfAbsConv f ≤ x := by
  cases x with
  | coe => exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h
  | top => exact le_top
  | bot =>
    refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
    cases y with
    | bot => simp at hy
    | coe y => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
    | top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩

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