English
If f is dominated by an integrable bound and g ∈ C(Y,E), the mapping x ↦ mkD (f x) g has finite integral.
Русский
Если f ограничена интегрируемым bound и g ∈ C(Y,E), то x ↦ mkD(f x) g имеет конечный интеграл.
LaTeX
$$$\text{HasFiniteIntegral}(x \mapsto \mathrm{mkD}(f(x), g), μ).$$$
Lean4
/-- A natural criterion for `HasFiniteIntegral` of a `C(Y, E)₀`-valued function is the existence
of some positive function with finite integral such that `∀ᵐ x ∂μ, ∀ y : Y, ‖f x y‖ ≤ bound x`.
Note that there is no dominated convergence here (hence no first-countability assumption
on `Y`). We are just using the properties of Banach-space-valued integration. -/
theorem hasFiniteIntegral_of_bound [CompactSpace Y] [Zero Y] (f : X → C(Y, E)₀) (bound : X → ℝ)
(bound_int : HasFiniteIntegral bound μ) (bound_ge : ∀ᵐ x ∂μ, ∀ y : Y, ‖f x y‖ ≤ bound x) : HasFiniteIntegral f μ :=
by
have bound_nonneg : 0 ≤ᵐ[μ] bound := by
filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x 0)
refine .mono' bound_int ?_
filter_upwards [bound_ge, bound_nonneg] with x bound_ge_x bound_nonneg_x
exact ContinuousMap.norm_le _ bound_nonneg_x |>.mpr bound_ge_x
