English
If f and g are integrable, then their pair is integrable (alternate presentation).
Русский
Если f и g интегрируемы, то их пара интегрируема (вариант формулировки).
LaTeX
$$$ (Integrable\\ f μ) \\land (Integrable\\ g μ) \\Rightarrow Integrable( x \\mapsto (f(x), g(x)) ) μ $$$
Lean4
theorem integrable_of_le_of_le {f g₁ g₂ : α → ℝ} (hf : AEStronglyMeasurable f μ) (h_le₁ : g₁ ≤ᵐ[μ] f)
(h_le₂ : f ≤ᵐ[μ] g₂) (h_int₁ : Integrable g₁ μ) (h_int₂ : Integrable g₂ μ) : Integrable f μ :=
by
have : ∀ᵐ x ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖ :=
by
filter_upwards [h_le₁, h_le₂] with x hx1 hx2
simp only [Real.norm_eq_abs]
exact abs_le_max_abs_abs hx1 hx2
have h_le_add : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖ :=
by
filter_upwards [this] with x hx
refine hx.trans ?_
conv_rhs => rw [Real.norm_of_nonneg (by positivity)]
exact max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)
exact Integrable.mono (by fun_prop) hf h_le_add
