lintegral_sub' — Mathlib

English

For g ≤ᵐ f with hg finite, the subtracted lintegrals satisfy ∫ (f − g) = ∫ f − ∫ g.

Русский

Если g ≤ᵐ f и hg конечен, то ∫ (f − g) = ∫ f − ∫ g.

LaTeX

$$$(hg : AEMeasurable\\ g\\ μ) \\wedge (hg\\_fin : ∫⁻ a, g(a) ∂μ ≠ ∞) \\Rightarrow ∫⁻ a, f(a) - g(a) ∂μ = ∫⁻ a, f(a) ∂μ - ∫⁻ a, g(a) ∂μ$$$

Lean4

theorem lintegral_sub' {f g : α → ℝ≥0∞} (hg : AEMeasurable g μ) (hg_fin : ∫⁻ a, g a ∂μ ≠ ∞) (h_le : g ≤ᵐ[μ] f) :
    ∫⁻ a, f a - g a ∂μ = ∫⁻ a, f a ∂μ - ∫⁻ a, g a ∂μ :=
  by
  refine ENNReal.eq_sub_of_add_eq hg_fin ?_
  rw [← lintegral_add_right' _ hg]
  exact lintegral_congr_ae (h_le.mono fun x hx => tsub_add_cancel_of_le hx)

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