English
If bound is integrable and, almost everywhere in μ, ∥f(xy)∥ ≤ bound(x) for all y ∈ Y, then f has finite integral.
Русский
Если bound интегрируем и почти что во всех x выполняется ∥f(x y)∥ ≤ bound(x) для всех y, тогда f имеет конечный интеграл.
LaTeX
$$$\text{HasFiniteIntegral}(f, μ)\text{ if } bound\in L^1(μ)\text{ and } ∀^{×} x, ∀ y, \|f(x,y)\| ≤ bound(x).$$$
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] (f : X → C(Y, E)) (bound : X → ℝ)
(bound_int : HasFiniteIntegral bound μ) (bound_ge : ∀ᵐ x ∂μ, ∀ y : Y, ‖f x y‖ ≤ bound x) : HasFiniteIntegral f μ :=
by
rcases isEmpty_or_nonempty Y with (h | h)
· simp
· have bound_nonneg : 0 ≤ᵐ[μ] bound := by
filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x h.some)
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
