box_integral_eq_integral — Mathlib

English

For a simple function f, its Box integral equals its standard measure integral over the restricted domain.

Русский

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

LaTeX

$$$$ BoxIntegral.integral I l f = \int_{\mu|_I} f $$$$

Lean4

/-- For a simple function, its McShane (or Henstock, or `⊥`) box integral is equal to its
integral in the sense of `MeasureTheory.SimpleFunc.integral`. -/
theorem box_integral_eq_integral (f : SimpleFunc (ι → ℝ) E) (μ : Measure (ι → ℝ)) [IsLocallyFiniteMeasure μ] (I : Box ι)
    (l : IntegrationParams) (hl : l.bRiemann = false) :
    BoxIntegral.integral.{u, v, v} I l f μ.toBoxAdditive.toSMul = f.integral (μ.restrict I) :=
  (f.hasBoxIntegral μ I l hl).integral_eq

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