English
The modified function f_modif, on the positive real axis, is locally integrable; this is shown by splitting into integrable components and using known local integrability of the base terms f, g₀ and the integrable modifications.
Русский
Локально интегрируема модификация f_modif на положительной оси; доказательство разделяет на интегрируемые части и использует локальную интегрируемость базовых членов.
LaTeX
$$LocallyIntegrableOn P.f_modif (Ioi 0)$$
Lean4
theorem hf_modif_int : LocallyIntegrableOn P.f_modif (Ioi 0) :=
by
have : LocallyIntegrableOn (fun x : ℝ ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) :=
by
refine ContinuousOn.locallyIntegrableOn ?_ measurableSet_Ioi
refine continuousOn_of_forall_continuousAt (fun x (hx : 0 < x) ↦ ?_)
refine (continuousAt_const.mul ?_).smul continuousAt_const
exact continuous_ofReal.continuousAt.comp (continuousAt_rpow_const _ _ (Or.inl hx.ne'))
refine LocallyIntegrableOn.add (fun x hx ↦ ?_) (fun x hx ↦ ?_)
· obtain ⟨s, hs, hs'⟩ := P.hf_int.sub (locallyIntegrableOn_const _) x hx
refine ⟨s, hs, ?_⟩
rw [IntegrableOn, integrable_indicator_iff measurableSet_Ioi, IntegrableOn,
Measure.restrict_restrict measurableSet_Ioi, ← IntegrableOn]
exact hs'.mono_set Set.inter_subset_right
· obtain ⟨s, hs, hs'⟩ := P.hf_int.sub this x hx
refine ⟨s, hs, ?_⟩
rw [IntegrableOn, integrable_indicator_iff measurableSet_Ioo, IntegrableOn,
Measure.restrict_restrict measurableSet_Ioo, ← IntegrableOn]
exact hs'.mono_set Set.inter_subset_right
