case pos
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g✝ : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
g : (ι → ℝ) → ℝ
hg : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → 0 ≤ g x
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : Integrable I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
⊢ 0 ≤ integral I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))

case neg
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g✝ : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
g : (ι → ℝ) → ℝ
hg : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → 0 ≤ g x
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : ¬Integrable I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
⊢ 0 ≤ integral I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g✝ : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
g : (ι → ℝ) → ℝ
hg : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → 0 ≤ g x
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ 0 ≤ integral I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
by_cases hgi : Integrable I l g μ.toBoxAdditive.toSMul
case pos
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J✝ : Box ι
π✝ : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g✝ : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
g : (ι → ℝ) → ℝ
hg : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → 0 ≤ g x
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : Integrable I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
π : TaggedPrepartition I
J : Box ι
x✝ : J ∈ π.boxes
⊢ 0 ≤ ↑(↑(BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) J) (g (tag π J))
case pos
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g✝ : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
g : (ι → ℝ) → ℝ
hg : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → 0 ≤ g x
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : Integrable I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
⊢ 0 ≤ integral I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
refine ge_of_tendsto' hgi.hasIntegral fun π => sum_nonneg fun J _ => ?_
no goals
case pos
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J✝ : Box ι
π✝ : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g✝ : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
g : (ι → ℝ) → ℝ
hg : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → 0 ≤ g x
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : Integrable I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
π : TaggedPrepartition I
J : Box ι
x✝ : J ∈ π.boxes
⊢ 0 ≤ ↑(↑(BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) J) (g (tag π J))
exact mul_nonneg ENNReal.toReal_nonneg (hg _ <| π.tag_mem_Icc _)
no goals
case neg
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g✝ : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
g : (ι → ℝ) → ℝ
hg : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → 0 ≤ g x
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : ¬Integrable I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
⊢ 0 ≤ integral I l g (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
rw [integral, dif_neg hgi]