integral_eq_lintegral — Mathlib

English

If f is a real-valued L1-simple function with 0 ≤ᵐ μ toSimpleFunc f, then the L1 integral equals the real of the lintegral of ENNReal.ofReal of toSimpleFunc f: ∫ f = toReal (∫⁻ ENNReal.ofReal ((toSimpleFunc f) ) dμ ).

Русский

Пусть f — вещественная простая функция в L1 и 0 ≤ᵐ μ toSimpleFunc f. Тогда интеграл L1 равен вещественной части линеграла: ∫ f = toReal (∫⁻ ENNReal.ofReal ((toSimpleFunc f)) dμ).

LaTeX

$$$\int f \, d\mu = \mathrm{ENNReal.toReal}\left(\int^{-} a, \mathrm{ENNReal.ofReal}((\mathrm{toSimpleFunc}\, f)(a)) \, d\mu(a)\right)$$$

Lean4

nonrec theorem integral_eq_lintegral {f : α →₁ₛ[μ] ℝ} (h_pos : 0 ≤ᵐ[μ] toSimpleFunc f) :
    integral f = ENNReal.toReal (∫⁻ a, ENNReal.ofReal ((toSimpleFunc f) a) ∂μ) := by
  rw [integral, SimpleFunc.integral_eq_lintegral (SimpleFunc.integrable f) h_pos]

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