integral_add_measure — Mathlib

English

Let f be a simple function nonnegative a.e. and μ ≤ ν; if f is integrable w.r.t ν, then the μ-integral is at most the ν-integral.

Русский

Пускай f неотрицательна почти повсюду и μ ≤ ν; если f интегрируема по ν, тогда μ-интеграл не превосходит ν-интеграла.

LaTeX

$$$$ f^{\\_integral}(μ) \\leq f^{\\_integral}(ν) \\quad\\text{when } μ \\le ν \\text{ and } f \\text{ integrable w.r.t } ν. $$$$

Lean4

theorem integral_add_measure {ν} (f : α →ₛ E) (hf : Integrable f (μ + ν)) :
    f.integral (μ + ν) = f.integral μ + f.integral ν :=
  by
  simp_rw [integral_def]
  refine setToSimpleFunc_add_left' (weightedSMul μ) (weightedSMul ν) (weightedSMul (μ + ν)) (fun s _ hμνs => ?_) hf
  rw [lt_top_iff_ne_top, Measure.coe_add, Pi.add_apply, ENNReal.add_ne_top] at hμνs
  rw [weightedSMul_add_measure _ _ hμνs.1 hμνs.2]

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