English
The complex power function x^r is interval-integrable on [a,b] under a suitable condition on r and the interval.
Русский
Функция x^r комплексной степени интегрируема на [a,b] при допустимом условии на r и интервал.
LaTeX
$$$\forall a,b\in\mathbb{R},\forall r\in\mathbb{C},\text{ если } \text{условие: }(0\in[ a,b] \Rightarrow \Re(r)<0) \Rightarrow \text{IntervalIntegrable } x^{r}$$$
Lean4
/-- See `intervalIntegrable_cpow'` for a version with a weaker hypothesis on `r`, but assuming the
measure is volume. -/
theorem intervalIntegrable_cpow {r : ℂ} (h : 0 ≤ r.re ∨ (0 : ℝ) ∉ [[a, b]]) :
IntervalIntegrable (fun x : ℝ => (x : ℂ) ^ r) μ a b :=
by
by_cases h2 : (0 : ℝ) ∉ [[a, b]]
· -- Easy case #1: 0 ∉ [a, b] -- use continuity.
refine (continuousOn_of_forall_continuousAt fun x hx => ?_).intervalIntegrable
exact Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_mem_of_not_mem hx h2)
rw [eq_false h2, or_false] at h
rcases lt_or_eq_of_le h with (h' | h')
· -- Easy case #2: 0 < re r -- again use continuity
exact
(Complex.continuous_ofReal_cpow_const h').intervalIntegrable _
_
-- Now the hard case: re r = 0 and 0 is in the interval.
refine (IntervalIntegrable.intervalIntegrable_norm_iff ?_).mp ?_
· refine (measurable_of_continuousOn_compl_singleton (0 : ℝ) ?_).aestronglyMeasurable
exact
continuousOn_of_forall_continuousAt fun x hx =>
Complex.continuousAt_ofReal_cpow_const x r
(Or.inr hx)
-- reduce to case of integral over `[0, c]`
suffices ∀ c : ℝ, IntervalIntegrable (fun x : ℝ => ‖(x : ℂ) ^ r‖) μ 0 c from (this a).symm.trans (this b)
intro c
rcases le_or_gt 0 c with (hc | hc)
· -- case `0 ≤ c`: integrand is identically 1
have : IntervalIntegrable (fun _ => 1 : ℝ → ℝ) μ 0 c := intervalIntegrable_const
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc] at this ⊢
refine IntegrableOn.congr_fun this (fun x hx => ?_) measurableSet_Ioc
dsimp only
rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1, ← h', rpow_zero]
· -- case `c < 0`: integrand is identically constant, *except* at `x = 0` if `r ≠ 0`.
apply IntervalIntegrable.symm
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc.le]
rw [← Ioo_union_right hc, integrableOn_union, and_comm]; constructor
·
exact
integrableOn_singleton (by simp) <|
isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_singleton
· have : ∀ x : ℝ, x ∈ Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖(x : ℂ) ^ r‖ :=
by
intro x hx
rw [Complex.ofReal_cpow_of_nonpos hx.2.le, norm_mul, ← Complex.ofReal_neg,
Complex.norm_cpow_eq_rpow_re_of_pos (neg_pos.mpr hx.2), ← h', rpow_zero, one_mul]
refine IntegrableOn.congr_fun ?_ this measurableSet_Ioo
rw [integrableOn_const_iff]
right
refine (measure_mono Set.Ioo_subset_Icc_self).trans_lt ?_
exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_Icc
