integral_of_fun_eq_integral' — Mathlib

English

Relates the L1-representation to the integral of f: the integral of a certain simpleq represented function equals the integral of f.

Русский

Связано с представлением в L1: интеграл некоторой функции равен интегралу от f.

LaTeX

$$$\text{MeasureTheory.}\text{integral}_μ (\text{AEEqFun.mk } f) = \int a, f(a) \partial μ$$$

Lean4

@[simp]
theorem integral_of_fun_eq_integral' {f : α → G} (hf : Integrable f μ) :
    ∫ a, (AEEqFun.mk f hf.aestronglyMeasurable) a ∂μ = ∫ a, f a ∂μ :=
  by
  by_cases hG : CompleteSpace G
  · simp only [MeasureTheory.integral, hG, L1.integral]
    exact setToFun_toL1 (dominatedFinMeasAdditive_weightedSMul μ) hf
  · simp [MeasureTheory.integral, hG]

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