Documentation

Mathlib.Analysis.BoxIntegral.Partition.Measure

Box-additive functions defined by measures #

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

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.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 μ] :
(μ (BoxIntegral.Prepartition.iUnion π)).toReal = Finset.sum π.boxes fun (J : BoxIntegral.Box ι) => (μ J).toReal

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

Equations
Instances For
    theorem BoxIntegral.Box.volume_apply {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) :
    (MeasureTheory.Measure.toBoxAdditive MeasureTheory.volume) I = Finset.prod Finset.univ fun (i : ι) => I.upper i - I.lower i
    @[simp]
    theorem BoxIntegral.Box.volume_apply' {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) :
    (MeasureTheory.volume I).toReal = Finset.prod Finset.univ fun (i : ι) => I.upper i - I.lower i
    theorem BoxIntegral.Box.volume_face_mul {n : } (i : Fin (n + 1)) (I : BoxIntegral.Box (Fin (n + 1))) :
    (Finset.prod Finset.univ fun (j : Fin n) => (BoxIntegral.Box.face I i).upper j - (BoxIntegral.Box.face I i).lower j) * (I.upper i - I.lower i) = Finset.prod Finset.univ fun (j : Fin (n + 1)) => I.upper j - I.lower j

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

    Equations
    Instances For
      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 : ι) => I.upper j - I.lower j) x