integral_eq_integral_pos_part_sub_integral_neg_part

English

For a SimpleFunc f: α → E, if f is integrable, then f.integral μ equals the Bochner integral of f, i.e., ∫ f = ∫ x f(x) dμ.

Русский

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

LaTeX

$$$f:\\alpha\\to E\\; (Integrable\\ f)\\;\\Rightarrow\\; f^{\\text{integral}}\\;=\\;\\int x\\, f(x)\\,d\\mu$$$

Lean4

theorem integral_eq_integral_pos_part_sub_integral_neg_part {f : α → ℝ} (hf : Integrable f μ) :
    ∫ a, f a ∂μ = ∫ a, (Real.toNNReal (f a) : ℝ) ∂μ - ∫ a, (Real.toNNReal (-f a) : ℝ) ∂μ :=
  by
  rw [← integral_sub hf.real_toNNReal]
  · simp
  · exact hf.neg.real_toNNReal

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