English
The reciprocal function f(x) on an interval avoiding zero is interval-integrable.
Русский
Обратная функция на интервале, не включающем ноль, интегрируема по интервалу.
LaTeX
$$$\forall a,b, 0\notin[a,b]: \text{IntervalIntegrable } x \mapsto x^{-1}$$$
Lean4
/-- See `intervalIntegrable_cpow` for a version applying to any locally finite measure, but with a
stronger hypothesis on `r`. -/
theorem intervalIntegrable_cpow' {r : ℂ} (h : -1 < r.re) : IntervalIntegrable (fun x : ℝ => (x : ℂ) ^ r) volume a b :=
by
suffices ∀ c : ℝ, IntervalIntegrable (fun x => (x : ℂ) ^ r) volume 0 c by
exact IntervalIntegrable.trans (this a).symm (this b)
have : ∀ c : ℝ, 0 ≤ c → IntervalIntegrable (fun x => (x : ℂ) ^ r) volume 0 c :=
by
intro c hc
rw [← IntervalIntegrable.intervalIntegrable_norm_iff]
· rw [intervalIntegrable_iff]
apply IntegrableOn.congr_fun
· rw [← intervalIntegrable_iff]; exact intervalIntegral.intervalIntegrable_rpow' h
· intro x hx
rw [uIoc_of_le hc] at hx
dsimp only
rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1]
· exact measurableSet_uIoc
· refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_uIoc
refine continuousOn_of_forall_continuousAt fun x hx => ?_
rw [uIoc_of_le hc] at hx
refine (continuousAt_cpow_const (Or.inl ?_)).comp Complex.continuous_ofReal.continuousAt
rw [Complex.ofReal_re]
exact hx.1
intro c; rcases le_total 0 c with (hc | hc)
· exact this c hc
· rw [IntervalIntegrable.iff_comp_neg, neg_zero]
have m := (this (-c) (by linarith)).const_mul (Complex.exp (π * Complex.I * r))
rw [intervalIntegrable_iff, uIoc_of_le (by linarith : 0 ≤ -c)] at m ⊢
refine m.congr_fun (fun x hx => ?_) measurableSet_Ioc
dsimp only
have : -x ≤ 0 := by linarith [hx.1]
rw [Complex.ofReal_cpow_of_nonpos this, mul_comm]
simp
