English
If f: R^n → E is almost everywhere continuous and bounded on a rectangular box I, then it is Box-integrable on I with respect to a locally finite μ, with the same integral.
Русский
Если f: R^n → E а.е. непрерывна и ограничена на коробке I, то по отношению к локально конечной мере μ fBox-интегрируема на I и интеграл совпадает.
LaTeX
$$$\text{HasIntegral}(I, l, f, \mu^{toBoxAdditive}, \int_{x \in I} f(x) \, d\mu)$$$
Lean4
/-- If `f : ℝⁿ → E` is a.e. continuous and bounded 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 ι}
(hb : ∃ C : ℝ, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C) (hc : ∀ᵐ x ∂μ, ContinuousAt f x) (l : IntegrationParams) :
HasIntegral.{u, v, v} I l f μ.toBoxAdditive.toSMul (∫ x in I, f x ∂μ) :=
by
obtain ⟨y, hy⟩ := integrable_of_bounded_and_ae_continuous l hb μ hc
convert hy
refine HasIntegral.unique (IntegrableOn.hasBoxIntegral ?_ ⊥ rfl) (HasIntegral.mono hy bot_le)
constructor
· let v := {x : (ι → ℝ) | ContinuousAt f x}
have : AEStronglyMeasurable f (μ.restrict v) :=
(continuousOn_of_forall_continuousAt fun _ h ↦ h).aestronglyMeasurable (measurableSet_of_continuousAt f)
refine this.mono_measure (Measure.le_iff.2 fun s hs ↦ ?_)
repeat rw [μ.restrict_apply hs]
apply le_of_le_of_eq <| μ.mono s.inter_subset_left
refine measure_eq_measure_of_null_diff s.inter_subset_left ?_ |>.symm
rw [diff_self_inter, Set.diff_eq]
refine (le_antisymm (zero_le (μ (s ∩ vᶜ))) ?_).symm
exact le_trans (μ.mono s.inter_subset_right) (nonpos_iff_eq_zero.2 hc)
· have : IsFiniteMeasure (μ.restrict (Box.Icc I)) :=
{ measure_univ_lt_top := by simp [I.isCompact_Icc.measure_lt_top (μ := μ)] }
have : IsFiniteMeasure (μ.restrict I) :=
isFiniteMeasure_of_le (μ.restrict (Box.Icc I)) (μ.restrict_mono Box.coe_subset_Icc (le_refl μ))
obtain ⟨C, hC⟩ := hb
refine .of_bounded (C := C) (Filter.eventually_iff_exists_mem.2 ?_)
use I, self_mem_ae_restrict I.measurableSet_coe, fun y hy ↦ hC y (I.coe_subset_Icc hy)
