English
Let f: R^n → E be continuous on a rectangular box I and μ a locally finite measure. Then f is Box-integrable on I with the same integral, i.e., the integral over I exists and equals ∫_I f dμ.
Русский
Пусть f: R^n → E непрерывна на прямоугольнике I и μ — locally finite мера. Тогда f является Box-интегрируемой по I с тем же интегралом, т.е. интеграл по I существует и равен ∫_I f dμ.
LaTeX
$$$\text{HasIntegral}(I, l, f, \mu^{toBoxAdditive}, \int_{x \in I} f(x) \, d\mu)$$$
Lean4
/-- If `f : ℝⁿ → E` is continuous on a rectangular box `I`, then it is Box integrable on `I`
w.r.t. a locally finite measure `μ` with the same integral. -/
theorem hasBoxIntegral [CompleteSpace E] {f : (ι → ℝ) → E} (μ : Measure (ι → ℝ)) [IsLocallyFiniteMeasure μ] {I : Box ι}
(hc : ContinuousOn f (Box.Icc I)) (l : IntegrationParams) :
HasIntegral.{u, v, v} I l f μ.toBoxAdditive.toSMul (∫ x in I, f x ∂μ) :=
by
obtain ⟨y, hy⟩ := BoxIntegral.integrable_of_continuousOn l hc μ
convert hy
have : IntegrableOn f I μ := IntegrableOn.mono_set (hc.integrableOn_compact I.isCompact_Icc) Box.coe_subset_Icc
exact HasIntegral.unique (IntegrableOn.hasBoxIntegral this ⊥ rfl) (HasIntegral.mono hy bot_le)
