bdd_mul' — Mathlib

English

If g is integrable and f is AEStronglyMeasurable with an a.e. bounded bound by c, then f g is integrable.

Русский

Если g интегрируем, f AEStronglyMeasurable и почти везде ограничен пределом c, то f g интегрируемо.

LaTeX

$$$\mathrm{Integrable}(g,\mu) \Rightarrow \mathrm{AEStronglyMeasurable}(f,\mu) \Rightarrow (|f| ≤ c \text{ a.e.}) \Rightarrow \mathrm{Integrable}(x \mapsto f(x)g(x),\mu).$$$

Lean4

theorem bdd_mul' {f g : α → 𝕜} {c : ℝ} (hg : Integrable g μ) (hf : AEStronglyMeasurable f μ)
    (hf_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) : Integrable (fun x => f x * g x) μ :=
  by
  refine Integrable.mono' (hg.norm.smul c) (hf.mul hg.1) ?_
  filter_upwards [hf_bound] with x hx
  rw [Pi.smul_apply, smul_eq_mul]
  exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right hx (norm_nonneg _))

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