prodMk — Mathlib

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 _⟩

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