hasFiniteIntegral_mkD_of_bound — Mathlib

English

If f is bounded by an integrable bound and g ∈ C(Y,E), then the function 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 variant of `ContinuousMap.hasFiniteIntegral_of_bound` spelled in terms of
`ContinuousMap.mkD`. -/
theorem hasFiniteIntegral_mkD_of_bound [CompactSpace Y] (f : X → Y → E) (g : C(Y, E))
    (f_ae_cont : ∀ᵐ x ∂μ, Continuous (f x)) (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] with x bound_ge_x cont_x
  simpa only [mkD_apply_of_continuous cont_x] using bound_ge_x

Похожие утверждения