integrable_right_of_integrable_add_of_nonneg

English

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

Русский

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

LaTeX

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

Lean4

theorem integrable_right_of_integrable_add_of_nonneg {f g : α → ℝ} (h_meas : AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f)
    (hg : 0 ≤ᵐ[μ] g) (h_int : Integrable (f + g) μ) : Integrable g μ :=
  integrable_left_of_integrable_add_of_nonneg
    ((AEStronglyMeasurable.add_iff_right h_meas).mp h_int.aestronglyMeasurable) hg hf (add_comm f g ▸ h_int)

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