English
Pairwise integrability theorem variant: the product pair is integrable.
Русский
Вариант теоремы о интегрируемости пары.
LaTeX
$$$ (Integrable\\ f μ) \\land (Integrable\\ g μ) \\Rightarrow Integrable( x \\mapsto (f(x), g(x)) ) μ $$$
Lean4
@[fun_prop]
theorem prodMk {f : α → β} {g : α → γ} (hf : Integrable f μ) (hg : Integrable g μ) :
Integrable (fun x => (f x, g x)) μ :=
⟨by fun_prop,
(hf.norm.add' hg.norm).mono <|
Eventually.of_forall fun x =>
calc
max ‖f x‖ ‖g x‖ ≤ ‖f x‖ + ‖g x‖ := max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)
_ ≤ ‖‖f x‖ + ‖g x‖‖ := le_abs_self _⟩