English
If a function f is bounded on box I and a.e. continuous with respect to μ on Box.Icc I, then f is Integrable on I with respect to μ.
Русский
Если функция f ограничена на I и почти всюду непрерывна относительно μ на Box.Icc I, то f интегрируема на I относительно μ.
LaTeX
$$$$\\text{Integrable}(I, l, f, μ.toBoxAdditive.toSMul).$$$$
Lean4
/-- A function that is bounded on a box `I` and a.e. continuous is integrable on `I`.
This is a version of `integrable_of_bounded_and_ae_continuousWithinAt` with a stronger continuity
assumption so that the user does not need to specialize the continuity assumption to each box on
which the theorem is to be applied. -/
theorem integrable_of_bounded_and_ae_continuous [CompleteSpace E] {I : Box ι} {f : ℝⁿ → E}
(hb : ∃ C : ℝ, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C) (μ : Measure ℝⁿ) [IsLocallyFiniteMeasure μ]
(hc : ∀ᵐ x ∂μ, ContinuousAt f x) : Integrable I l f μ.toBoxAdditive.toSMul :=
integrable_of_bounded_and_ae_continuousWithinAt l hb μ <|
Eventually.filter_mono (ae_mono μ.restrict_le_self) (hc.mono fun _ h ↦ h.continuousWithinAt)
