integrableAtFilter_rpow_atTop_iff

English

For s, integrability at infinity along the power function is equivalent to s < -1.

Русский

Для параметра s интегрируемость при бесконечности для x^s равнозначна s < -1.

LaTeX

$$$\\text{IntegrableAtFilter} \\big( x \\mapsto x^{s} \\big) \\text{ atTop} \\iff s < -1$$$

Lean4

theorem integrableAtFilter_rpow_atTop_iff {s : ℝ} : IntegrableAtFilter (fun x : ℝ ↦ x ^ s) atTop ↔ s < -1 :=
  by
  refine ⟨fun ⟨t, ht, hint⟩ ↦ ?_, fun h ↦ ⟨Set.Ioi 1, Ioi_mem_atTop 1, (integrableOn_Ioi_rpow_iff zero_lt_one).mpr h⟩⟩
  obtain ⟨a, ha⟩ := mem_atTop_sets.mp ht
  refine (integrableOn_Ioi_rpow_iff (zero_lt_one.trans_le (le_max_right a 1))).mp ?_
  exact hint.mono_set <| fun x hx ↦ ha _ <| (le_max_left a 1).trans hx.le

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