English
Analogous variant for ContinuousMapZero; dominated by an integrable bound implies HasFiniteIntegral of x ↦ mkD.
Русский
Аналогично вариации для ContinuousMapZero: если имеется интегрируемое доминирующее bound, то HasFiniteIntegral mkD.
LaTeX
$$$\text{HasFiniteIntegral}(x \mapsto \mathrm{mkD}(f(x), g), μ).$$$
Lean4
/-- A variant of `ContinuousMapZero.hasFiniteIntegral_of_bound` spelled in terms of
`ContinuousMapZero.mkD`. -/
theorem hasFiniteIntegral_mkD_of_bound [CompactSpace Y] [Zero Y] (f : X → Y → E) (g : C(Y, E)₀)
(f_ae_cont : ∀ᵐ x ∂μ, Continuous (f x)) (f_ae_zero : ∀ᵐ x ∂μ, f x 0 = 0) (bound : X → ℝ)
(bound_int : HasFiniteIntegral bound μ) (bound_ge : ∀ᵐ x ∂μ, ∀ y : Y, ‖f x y‖ ≤ bound x) :
HasFiniteIntegral (fun x ↦ mkD (f x) g) μ :=
by
refine hasFiniteIntegral_of_bound _ bound bound_int ?_
filter_upwards [bound_ge, f_ae_cont, f_ae_zero] with x bound_ge_x cont_x zero_x
simpa only [mkD_apply_of_continuous cont_x zero_x] using bound_ge_x
