integral_eq_integral — Mathlib

English

For a simple function f: α → E, if f is integrable, then its Bochner integral equals the ordinary integral of f with respect to μ.

Русский

Для простой функции f: α → E, интегрируемой, интеграл Бо́хнера равен обычному интегралу по μ.

LaTeX

$$$\\text{If } f:\\alpha\\to E\\text{ is simple and integrable, then } f_{\\text{integral}} = \\int x\\, f(x)\\,d\\mu$.$$

Lean4

theorem integral_eq_integral (f : α →ₛ E) (hfi : Integrable f μ) : f.integral μ = ∫ x, f x ∂μ :=
  by
  rw [MeasureTheory.integral_eq f hfi, ← L1.SimpleFunc.toLp_one_eq_toL1, L1.SimpleFunc.integral_L1_eq_integral,
    L1.SimpleFunc.integral_eq_integral]
  exact SimpleFunc.integral_congr hfi (Lp.simpleFunc.toSimpleFunc_toLp _ _).symm

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