abscissaOfAbsConv_le_of_isBigO_rpow

English

If f = O(n^x), then abscissaOfAbsConv f ≤ x+1.

Русский

Если f = O(n^x), то abscissaOfAbsConv f ≤ x+1.

LaTeX

$$$\\text{If } f =O\\big(n^{x}\\big)\\text{, then } \\operatorname{abscissaOfAbsConv}(f) \\le x+1.$$$

Lean4

/-- If `‖f n‖` is `O(n^x)`, then the abscissa of absolute convergence
of `f` is bounded by `x + 1`. -/
theorem abscissaOfAbsConv_le_of_isBigO_rpow {f : ℕ → ℂ} {x : ℝ} (h : f =O[atTop] fun n ↦ (n : ℝ) ^ x) :
    abscissaOfAbsConv f ≤ x + 1 := by
  rw [show x = x + 1 - 1 by ring] at h
  by_contra! H
  obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H
  exact
    (LSeriesSummable_of_isBigO_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h |>.abscissaOfAbsConv_le.trans_lt hy₂).false

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