English
For t > 0, integrability of x^s on (t, ∞) is equivalent to s < -1.
Русский
При t > 0 интегрируемость x^s на (t, ∞) эквивалентна s < -1.
LaTeX
$$$\\text{IntegrableOn} (x \\mapsto x^{s}) (Ioi\\ t) \\iff s < -1$, $t>0$$$
Lean4
theorem integrableOn_Ioi_rpow_iff {s t : ℝ} (ht : 0 < t) : IntegrableOn (fun x ↦ x ^ s) (Ioi t) ↔ s < -1 :=
by
refine ⟨fun h ↦ ?_, fun h ↦ integrableOn_Ioi_rpow_of_lt h ht⟩
contrapose! h
intro H
have H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) := H.mono (Set.Ioi_subset_Ioi (le_max_right _ _)) le_rfl
have : IntegrableOn (fun x ↦ x⁻¹) (Ioi (max 1 t)) :=
by
apply H'.mono' measurable_inv.aestronglyMeasurable
filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
have x_one : 1 ≤ x := ((le_max_left _ _).trans_lt (mem_Ioi.1 hx)).le
simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans x_one)]
rw [← Real.rpow_neg_one x]
exact Real.rpow_le_rpow_of_exponent_le x_one h
exact not_IntegrableOn_Ioi_inv this
