ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
y : E
f g : (ι → ℝ) → E
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hf : HasIntegral I l f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) y
hfg : f =ᵐ[Measure.restrict μ ↑I] g
hl : l.bRiemann = false
this : g - f =ᵐ[Measure.restrict μ ↑I] 0
⊢ HasIntegral I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) y
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
y : E
f g : (ι → ℝ) → E
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hf : HasIntegral I l f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) y
hfg : f =ᵐ[Measure.restrict μ ↑I] g
hl : l.bRiemann = false
⊢ HasIntegral I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) y
have : g - f =ᵐ[μ.restrict I] 0 := hfg.mono fun x hx => sub_eq_zero.2 hx.symm
no goals
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
y : E
f g : (ι → ℝ) → E
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hf : HasIntegral I l f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) y
hfg : f =ᵐ[Measure.restrict μ ↑I] g
hl : l.bRiemann = false
this : g - f =ᵐ[Measure.restrict μ ↑I] 0
⊢ HasIntegral I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) y
simpa using hf.add (HasIntegral.of_aeEq_zero this hl)