mathlib documentation


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 box_integral.box_additive function.

Tags #

rectangular box, measure

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

theorem {ι : Type u_1} [fintype ι] (I : ι) :
theorem {n : } (i : fin (n + 1)) (I : (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)
noncomputable def box_integral.box_additive_map.volume {ι : Type u_1} [fintype ι] {E : Type u_2} [normed_group E] [normed_space E] :

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

theorem box_integral.box_additive_map.volume_apply {ι : Type u_1} [fintype ι] {E : Type u_2} [normed_group E] [normed_space E] (I : ι) (x : E) :
(box_integral.box_additive_map.volume I) x = (∏ (j : ι), (I.upper j - I.lower j)) x