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 : BoxIntegral.Box ι) (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ] : ↑↑μ (↑BoxIntegral.Box.Icc I) < ⊤

theorem BoxIntegral.Box.measure_coe_lt_top {ι : Type u_1} (I : BoxIntegral.Box ι) (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ] : ↑↑μ ↑I < ⊤

theorem BoxIntegral.Box.measurableSet_coe {ι : Type u_1} (I : BoxIntegral.Box ι) [Countable ι] : MeasurableSet ↑I

theorem BoxIntegral.Box.measurableSet_Icc {ι : Type u_1} (I : BoxIntegral.Box ι) [Countable ι] : MeasurableSet (↑BoxIntegral.Box.Icc I)

theorem BoxIntegral.Box.measurableSet_Ioo {ι : Type u_1} (I : BoxIntegral.Box ι) [Countable ι] : MeasurableSet (↑BoxIntegral.Box.Ioo I)

theorem BoxIntegral.Box.coe_ae_eq_Icc {ι : Type u_1} (I : BoxIntegral.Box ι) [Fintype ι] : ↑I =ᶠ[MeasureTheory.Measure.ae MeasureTheory.volume] ↑BoxIntegral.Box.Icc I

theorem BoxIntegral.Box.Ioo_ae_eq_Icc {ι : Type u_1} (I : BoxIntegral.Box ι) [Fintype ι] : ↑BoxIntegral.Box.Ioo I =ᶠ[MeasureTheory.Measure.ae MeasureTheory.volume] ↑BoxIntegral.Box.Icc I

theorem BoxIntegral.Prepartition.measure_iUnion_toReal {ι : Type u_1} [Finite ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ] : ENNReal.toReal (↑↑μ (BoxIntegral.Prepartition.iUnion π)) = Finset.sum π.boxes fun J => ENNReal.toReal (↑↑μ ↑J)

@[simp]

theorem MeasureTheory.Measure.toBoxAdditive_apply {ι : Type u_1} [Fintype ι] (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ] (J : BoxIntegral.Box ι) : ↑(MeasureTheory.Measure.toBoxAdditive μ) J = ENNReal.toReal (↑↑μ ↑J)

def MeasureTheory.Measure.toBoxAdditive {ι : Type u_1} [Fintype ι] (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ] : BoxIntegral.BoxAdditiveMap ι ℝ ⊤

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

Equations

• One or more equations did not get rendered due to their size.

theorem BoxIntegral.Box.volume_apply {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) : ↑(MeasureTheory.Measure.toBoxAdditive MeasureTheory.volume) I = Finset.prod Finset.univ fun i => BoxIntegral.Box.upper I i - BoxIntegral.Box.lower I i

@[simp]

theorem BoxIntegral.Box.volume_apply' {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) : ENNReal.toReal (↑↑MeasureTheory.volume ↑I) = Finset.prod Finset.univ fun i => BoxIntegral.Box.upper I i - BoxIntegral.Box.lower I i

theorem BoxIntegral.Box.volume_face_mul {n : ℕ} (i : Fin (n + 1)) (I : BoxIntegral.Box (Fin (n + 1))) : (Finset.prod Finset.univ fun j => BoxIntegral.Box.upper (BoxIntegral.Box.face I i) j - BoxIntegral.Box.lower (BoxIntegral.Box.face I i) j) * (BoxIntegral.Box.upper I i - BoxIntegral.Box.lower I i) = Finset.prod Finset.univ fun j => BoxIntegral.Box.upper I j - BoxIntegral.Box.lower I j

def BoxIntegral.BoxAdditiveMap.volume {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] E) ⊤

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

Equations

• BoxIntegral.BoxAdditiveMap.volume = BoxIntegral.BoxAdditiveMap.toSMul (MeasureTheory.Measure.toBoxAdditive MeasureTheory.volume)

theorem BoxIntegral.BoxAdditiveMap.volume_apply {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (I : BoxIntegral.Box ι) (x : E) : ↑(↑BoxIntegral.BoxAdditiveMap.volume I) x = (Finset.prod Finset.univ fun j => BoxIntegral.Box.upper I j - BoxIntegral.Box.lower I j) • x