English
A variant of the previous result: with g ∈ C(Y,E) and bound integrable, if ∥f(x)∥ ≤ bound(x) a.e., then x ↦ mkD(f(x)) g has finite integral.
Русский
Вариант предыдущего: с g ∈ C(Y,E) и интегрируемым bound, если ∥f(x)∥ ≤ bound(x) а.е., то x ↦ mkD(f(x)) g имеет конечный интеграл.
LaTeX
$$$\text{HasFiniteIntegral}(x \mapsto \mathrm{mkD}(f(x), g), μ)\text{ if } bound∈L^1(μ)\ and \|f(x)\| ≤ bound(x)\ a.e.$$$
Lean4
/-- A variant of `ContinuousMap.hasFiniteIntegral_mkD_of_bound` for a family of
functions which are continuous on a compact set. -/
theorem hasFiniteIntegral_mkD_restrict_of_bound {s : Set Y} [CompactSpace s] (f : X → Y → E) (g : C(s, E))
(f_ae_contOn : ∀ᵐ x ∂μ, ContinuousOn (f x) s) (bound : X → ℝ) (bound_int : HasFiniteIntegral bound μ)
(bound_ge : ∀ᵐ x ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x) : HasFiniteIntegral (fun x ↦ mkD (s.restrict (f x)) g) μ :=
by
refine hasFiniteIntegral_mkD_of_bound _ _ ?_ bound bound_int ?_
· simpa [← continuousOn_iff_continuous_restrict]
· simpa
