English
If f is bounded and g is integrable, then f·g is integrable.
Русский
Если f ограничена и g интегрируема, то f·g интегрируемо.
LaTeX
$$$ \\exists C\\, \\forall x, \\|f(x)\\| \\le C \\land Integrable(g) μ \\Rightarrow Integrable( x\\mapsto f(x)\\,g(x) ) μ $$$
Lean4
theorem bdd_mul {F : Type*} [NormedDivisionRing F] {f g : α → F} (hint : Integrable g μ) (hm : AEStronglyMeasurable f μ)
(hfbdd : ∃ C, ∀ x, ‖f x‖ ≤ C) : Integrable (fun x => f x * g x) μ :=
by
rcases isEmpty_or_nonempty α with hα | hα
· rw [μ.eq_zero_of_isEmpty]
exact integrable_zero_measure
· refine ⟨hm.mul hint.1, ?_⟩
obtain ⟨C, hC⟩ := hfbdd
have hCnonneg : 0 ≤ C := le_trans (norm_nonneg _) (hC hα.some)
have : (fun x => ‖f x * g x‖₊) ≤ fun x => ⟨C, hCnonneg⟩ * ‖g x‖₊ :=
by
intro x
simp only [nnnorm_mul]
exact mul_le_mul_of_nonneg_right (hC x) (zero_le _)
refine lt_of_le_of_lt (lintegral_mono_nnreal this) ?_
simp only [ENNReal.coe_mul]
rw [lintegral_const_mul' _ _ ENNReal.coe_ne_top]
exact
ENNReal.mul_lt_top ENNReal.coe_lt_top
hint.2
-- TODO: generalise the following lemmas to enorm classes
