integral_of_fun_eq_integral — Mathlib

English

For integrable f, the L1-representation integrated equals the standard integral of f.

Русский

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

LaTeX

$$$\int a, (\text{Integrable.toL1 } f \; hf).val.cast a \, dμ = \int a, f(a) \, dμ$$$

Lean4

theorem integral_of_fun_eq_integral {f : α → G} (hf : Integrable f μ) : ∫ a, (hf.toL1 f) a ∂μ = ∫ a, f a ∂μ := by
  simp [hf]

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