English
The complex power x^r is interval-integrable on [a,b] for a,b ∈ ℝ and r ∈ ℂ with appropriate conditions.
Русский
Функция x^r комплексной степени интегрируема по интервалу [a,b] при допустимых условиях.
LaTeX
$$$\forall a,b\in\mathbb{R},\text{ IntervalIntegrable } (\lambda x. x^{r}) \text{ на }[a,b]$$$
Lean4
/-- The power function `x ↦ x^s` is integrable on `(0, t)` iff `-1 < s`. -/
theorem integrableOn_Ioo_rpow_iff {s t : ℝ} (ht : 0 < t) : IntegrableOn (fun x ↦ x ^ s) (Ioo (0 : ℝ) t) ↔ -1 < s :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
swap
· rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
apply intervalIntegrable_rpow' h (a := 0) (b := t)
contrapose! h
intro H
have I : 0 < min 1 t := lt_min zero_lt_one ht
have H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) :=
H.mono (Set.Ioo_subset_Ioo le_rfl (min_le_right _ _)) le_rfl
have : IntegrableOn (fun x ↦ x⁻¹) (Ioo 0 (min 1 t)) :=
by
apply H'.mono' measurable_inv.aestronglyMeasurable
filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx
simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hx.1)]
rwa [← Real.rpow_neg_one x, Real.rpow_le_rpow_left_iff_of_base_lt_one hx.1]
exact lt_of_lt_of_le hx.2 (min_le_left _ _)
have : IntervalIntegrable (fun x ↦ x⁻¹) volume 0 (min 1 t) := by
rwa [intervalIntegrable_iff_integrableOn_Ioo_of_le I.le]
simp [intervalIntegrable_inv_iff, I.ne] at this
