case h_ind
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
y : E
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ HasIntegral I l (↑(piecewise s hs (const (ι → ℝ) y) (const (ι → ℝ) 0)))
    (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
    (integral (Measure.restrict μ ↑I) (piecewise s hs (const (ι → ℝ) y) (const (ι → ℝ) 0)))

case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
⊢ HasIntegral I l (↑(f + g)) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
    (integral (Measure.restrict μ ↑I) (f + g))
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : SimpleFunc (ι → ℝ) E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
⊢ HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
induction' f using MeasureTheory.SimpleFunc.induction with y s hs f g _ hfi hgi
no goals
case h_ind
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
y : E
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ HasIntegral I l (↑(piecewise s hs (const (ι → ℝ) y) (const (ι → ℝ) 0)))
    (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
    (integral (Measure.restrict μ ↑I) (piecewise s hs (const (ι → ℝ) y) (const (ι → ℝ) 0)))
simpa only [Measure.restrict_apply hs, const_zero, integral_piecewise_zero, integral_const,
  Measure.restrict_apply, MeasurableSet.univ, Set.univ_inter] using
  BoxIntegral.hasIntegralIndicatorConst l hl hs I y μ
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ HasIntegral I l (↑(f + g)) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
    (integral (Measure.restrict μ ↑I) (f + g))
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
⊢ HasIntegral I l (↑(f + g)) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
    (integral (Measure.restrict μ ↑I) (f + g))
borelize E
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (↑↑μ ↑I < ⊤)
⊢ HasIntegral I l (↑(f + g)) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
    (integral (Measure.restrict μ ↑I) (f + g))
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ HasIntegral I l (↑(f + g)) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
    (integral (Measure.restrict μ ↑I) (f + g))
haveI := Fact.mk (I.measure_coe_lt_top μ)
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (↑↑μ ↑I < ⊤)
⊢ HasIntegral I l (↑(f + g)) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
    (integral (Measure.restrict μ ↑I) f + integral (Measure.restrict μ ↑I) g)

case h_add.hf
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (↑↑μ ↑I < ⊤)
⊢ Integrable ↑f

case h_add.hg
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (↑↑μ ↑I < ⊤)
⊢ Integrable ↑g
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (↑↑μ ↑I < ⊤)
⊢ HasIntegral I l (↑(f + g)) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
    (integral (Measure.restrict μ ↑I) (f + g))
rw [integral_add]
no goals
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (↑↑μ ↑I < ⊤)
⊢ HasIntegral I l (↑(f + g)) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
    (integral (Measure.restrict μ ↑I) f + integral (Measure.restrict μ ↑I) g)

case h_add.hf
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (↑↑μ ↑I < ⊤)
⊢ Integrable ↑f

case h_add.hg
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)
hfi : HasIntegral I l (↑f) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) f)
hgi : HasIntegral I l (↑g) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) (integral (Measure.restrict μ ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (↑↑μ ↑I < ⊤)
⊢ Integrable ↑g
exacts [hfi.add hgi, integrable_iff.2 fun _ _ => measure_lt_top _ _,
  integrable_iff.2 fun _ _ => measure_lt_top _ _]