integrable_of_norm_sub_le — Mathlib

English

If f and g are integrable, then the product-valued pair (f,g) is integrable.

Русский

Если f и g интегрируемы, то функция x ↦ (f(x), g(x)) интегрируема.

LaTeX

$$$ (Integrable\\ f μ) \\land (Integrable\\ g μ) \\Rightarrow Integrable( x \\mapsto (f(x), g(x)) ) μ $$$

Lean4

theorem integrable_of_norm_sub_le {f₀ f₁ : α → β} {g : α → ℝ} (hf₁_m : AEStronglyMeasurable f₁ μ)
    (hf₀_i : Integrable f₀ μ) (hg_i : Integrable g μ) (h : ∀ᵐ a ∂μ, ‖f₀ a - f₁ a‖ ≤ g a) : Integrable f₁ μ :=
  haveI : ∀ᵐ a ∂μ, ‖f₁ a‖ ≤ ‖f₀ a‖ + g a := by
    apply h.mono
    intro a ha
    calc
      ‖f₁ a‖ ≤ ‖f₀ a‖ + ‖f₀ a - f₁ a‖ := norm_le_insert _ _
      _ ≤ ‖f₀ a‖ + g a := add_le_add_left ha _
  Integrable.mono' (hf₀_i.norm.add hg_i) hf₁_m this

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