English
If a function equals zero almost everywhere on a box with respect to a locally finite measure, then its McShane integral on that box is zero.
Русский
Если функция равна нуль почти везде на коробке относительно локально конечной меры, то её McShane интеграл на этой коробке равен нулю.
LaTeX
$$$$ f =^\ae_{\mu|_I} 0 \Rightarrow HasIntegral I l f \mu^{toBoxAdditive} = 0. $$$$
Lean4
/-- If `f` has integral `y` on a box `I` with respect to a locally finite measure `μ` and `g` is
a.e. equal to `f` on `I`, then `g` has the same integral on `I`. -/
theorem congr_ae {l : IntegrationParams} {I : Box ι} {y : E} {f g : (ι → ℝ) → E} {μ : Measure (ι → ℝ)}
[IsLocallyFiniteMeasure μ] (hf : HasIntegral.{u, v, v} I l f μ.toBoxAdditive.toSMul y) (hfg : f =ᵐ[μ.restrict I] g)
(hl : l.bRiemann = false) : HasIntegral.{u, v, v} I l g μ.toBoxAdditive.toSMul y :=
by
have : g - f =ᵐ[μ.restrict I] 0 := hfg.mono fun x hx => sub_eq_zero.2 hx.symm
simpa using hf.add (HasIntegral.of_aeEq_zero this hl)
