# Box-additive functions defined by measures #

In this file we prove a few simple facts about rectangular boxes, partitions, and measures:

• given a box I : Box ι, its coercion to Set (ι → ℝ) and I.Icc are measurable sets;
• if μ is a locally finite measure, then (I : Set (ι → ℝ)) and I.Icc have finite measure;
• if μ is a locally finite measure, then fun J ↦ (μ J).toReal is a box additive function.

For the last statement, we both prove it as a proposition and define a bundled BoxIntegral.BoxAdditiveMap function.

## Tags #

rectangular box, measure

theorem BoxIntegral.Box.measure_Icc_lt_top {ι : Type u_1} (I : ) (μ : MeasureTheory.Measure (ι)) :
μ (BoxIntegral.Box.Icc I) <
theorem BoxIntegral.Box.measure_coe_lt_top {ι : Type u_1} (I : ) (μ : MeasureTheory.Measure (ι)) :
μ I <
theorem BoxIntegral.Box.measurableSet_coe {ι : Type u_1} (I : ) [] :
theorem BoxIntegral.Box.measurableSet_Icc {ι : Type u_1} (I : ) [] :
MeasurableSet (BoxIntegral.Box.Icc I)
theorem BoxIntegral.Box.measurableSet_Ioo {ι : Type u_1} (I : ) [] :
MeasurableSet (BoxIntegral.Box.Ioo I)
theorem BoxIntegral.Box.coe_ae_eq_Icc {ι : Type u_1} (I : ) [] :
I =ᵐ[MeasureTheory.volume] BoxIntegral.Box.Icc I
theorem BoxIntegral.Box.Ioo_ae_eq_Icc {ι : Type u_1} (I : ) [] :
BoxIntegral.Box.Ioo I =ᵐ[MeasureTheory.volume] BoxIntegral.Box.Icc I
theorem BoxIntegral.Prepartition.measure_iUnion_toReal {ι : Type u_1} [] {I : } (π : ) (μ : MeasureTheory.Measure (ι)) :
(μ π.iUnion).toReal = Jπ.boxes, (μ J).toReal
@[simp]
theorem MeasureTheory.Measure.toBoxAdditive_apply {ι : Type u_1} [] (μ : MeasureTheory.Measure (ι)) (J : ) :

If μ is a locally finite measure on ℝⁿ, then fun J ↦ (μ J).toReal is a box-additive function.

Equations
• μ.toBoxAdditive = { toFun := fun (J : ) => (μ J).toReal, sum_partition_boxes' := }
Instances For
theorem BoxIntegral.Box.volume_apply {ι : Type u_1} [] (I : ) :
MeasureTheory.volume.toBoxAdditive I = i : ι, (I.upper i - I.lower i)
@[simp]
theorem BoxIntegral.Box.volume_apply' {ι : Type u_1} [] (I : ) :
(MeasureTheory.volume I).toReal = i : ι, (I.upper i - I.lower i)
theorem BoxIntegral.Box.volume_face_mul {n : } (i : Fin (n + 1)) (I : BoxIntegral.Box (Fin (n + 1))) :
(j : Fin n, ((I.face i).upper j - (I.face i).lower j)) * (I.upper i - I.lower i) = j : Fin (n + 1), (I.upper j - I.lower j)
def BoxIntegral.BoxAdditiveMap.volume {ι : Type u_1} [] {E : Type u_2} [] :

Box-additive map sending each box I to the continuous linear endomorphism x ↦ (volume I).toReal • x.

Equations