integrable_left_of_integrable_add_of_nonneg

English

If f and g are nonnegative almost everywhere and f+g is integrable, then f is integrable.

Русский

Пусть f и g неотрицательны μ-почти всюду, и сумма f+g интегрируема; тогда f интегрируема.

LaTeX

$$$ (AEStronglyMeasurable\ f\ μ) \\land (0 \\le f)\\ a.e.\ μ \\land (0 \\le g)\\ a.e.\ μ \\land Integrable(f+g)\\ μ \\Rightarrow Integrable(f)\\ μ $$$

Lean4

theorem integrable_left_of_integrable_add_of_nonneg {f g : α → ℝ} (h_meas : AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f)
    (hg : 0 ≤ᵐ[μ] g) (h_int : Integrable (f + g) μ) : Integrable f μ :=
  by
  refine h_int.mono' h_meas ?_
  filter_upwards [hf, hg] with a haf hag
  exact (Real.norm_of_nonneg haf).symm ▸ le_add_of_nonneg_right hag

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