English
A restricted version: if t compact, f defined on X→Y→E, g ∈ C(t,E)₀, and a bound dominates on μ-restricted domain, then HasFiniteIntegral of the restricted mkD holds.
Русский
Ограниченная версия: если t компактно, f: X→Y→E, g ∈ C(t,E)₀ и имеется доминирование bound на μ-restricted домене, тогда HasFiniteIntegral mkD.
LaTeX
$$$\\text{HasFiniteIntegral}(x \\mapsto \\mathrm{mkD}(s.restrict(f x)) g, μ).$$$
Lean4
/-- A variant of `ContinuousMapZero.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] [Zero s] (f : X → Y → E) (g : C(s, E)₀)
(f_ae_contOn : ∀ᵐ x ∂μ, ContinuousOn (f x) s) (f_ae_zero : ∀ᵐ x ∂μ, f x (0 : s) = 0) (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 _ _ ?_ f_ae_zero bound bound_int ?_
· simpa [← continuousOn_iff_continuous_restrict]
· simpa
