English
If two Box integrals are taken with ae-equal data, then they yield equal results.
Русский
Если дваBox интеграла вычисляются на ae-эквивалентных данных, то они дают одинаковый результат.
LaTeX
$$$$\text{HasIntegral } I l f = \text{HasIntegral } I l g \quad (f =^\ae g).$$$$
Lean4
/-- A simple function is McShane integrable w.r.t. any locally finite measure. -/
theorem hasBoxIntegral (f : SimpleFunc (ι → ℝ) E) (μ : Measure (ι → ℝ)) [IsLocallyFiniteMeasure μ] (I : Box ι)
(l : IntegrationParams) (hl : l.bRiemann = false) :
HasIntegral.{u, v, v} I l f μ.toBoxAdditive.toSMul (f.integral (μ.restrict I)) := by
induction f using MeasureTheory.SimpleFunc.induction with
| @const y s hs => simpa [hs] using BoxIntegral.hasIntegralIndicatorConst l hl hs I y μ
| @add f g _ hfi hgi =>
borelize E; haveI := Fact.mk (I.measure_coe_lt_top μ)
rw [integral_add]
exacts [hfi.add hgi, integrable_iff.2 fun _ _ => measure_lt_top _ _, integrable_iff.2 fun _ _ => measure_lt_top _ _]
