Box-additive functions defined by measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 λ J, (μ J).to_real is a box additive function.

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

Tags #

rectangular box, measure

theorem box_integral.box.measure_Icc_lt_top {ι : Type u_1} (I : box_integral.box ι) (μ : measure_theory.measure (ι → ℝ)) [measure_theory.is_locally_finite_measure μ] :

⇑μ (⇑box_integral.box.Icc I) < ⊤

source

theorem box_integral.box.measure_coe_lt_top {ι : Type u_1} (I : box_integral.box ι) (μ : measure_theory.measure (ι → ℝ)) [measure_theory.is_locally_finite_measure μ] :

⇑μ ↑I < ⊤

source

theorem box_integral.box.measurable_set_coe {ι : Type u_1} (I : box_integral.box ι) [countable ι] :

measurable_set ↑I

source

theorem box_integral.box.measurable_set_Icc {ι : Type u_1} (I : box_integral.box ι) [countable ι] :

measurable_set (⇑box_integral.box.Icc I)

source

theorem box_integral.box.measurable_set_Ioo {ι : Type u_1} (I : box_integral.box ι) [countable ι] :

measurable_set (⇑box_integral.box.Ioo I)

source

theorem box_integral.box.coe_ae_eq_Icc {ι : Type u_1} (I : box_integral.box ι) [fintype ι] :

↑I =ᵐ[measure_theory.measure_space.volume ] ⇑box_integral.box.Icc I

source

theorem box_integral.box.Ioo_ae_eq_Icc {ι : Type u_1} (I : box_integral.box ι) [fintype ι] :

⇑box_integral.box.Ioo I =ᵐ[measure_theory.measure_space.volume ] ⇑box_integral.box.Icc I

source

theorem box_integral.prepartition.measure_Union_to_real {ι : Type u_1} [finite ι] {I : box_integral.box ι} (π : box_integral.prepartition I) (μ : measure_theory.measure (ι → ℝ)) [measure_theory.is_locally_finite_measure μ] :

(⇑μ π.Union).to_real = π.boxes.sum (λ (J : box_integral.box ι), (⇑μ ↑J).to_real)

source

@[simp]

theorem measure_theory.measure.to_box_additive_apply {ι : Type u_1} [fintype ι] (μ : measure_theory.measure (ι → ℝ)) [measure_theory.is_locally_finite_measure μ] (J : box_integral.box ι) :

⇑(μ.to_box_additive) J = (⇑μ ↑J).to_real

source

def measure_theory.measure.to_box_additive {ι : Type u_1} [fintype ι] (μ : measure_theory.measure (ι → ℝ)) [measure_theory.is_locally_finite_measure μ] :

box_integral.box_additive_map ι ℝ ⊤

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

Equations

μ.to_box_additive = {to_fun := λ (J : box_integral.box ι), (⇑μ ↑J).to_real, sum_partition_boxes' := _}

source

@[simp]

theorem box_integral.box.volume_apply {ι : Type u_1} [fintype ι] (I : box_integral.box ι) :

⇑(measure_theory.measure_space.volume.to_box_additive) I = finset.univ.prod (λ (i : ι), I.upper i - I.lower i)

source

theorem box_integral.box.volume_face_mul {n : ℕ} (i : fin (n + 1)) (I : box_integral.box (fin (n + 1))) :

finset.univ.prod (λ (j : fin n), (I.face i).upper j - (I.face i).lower j) * (I.upper i - I.lower i) = finset.univ.prod (λ (j : fin (n + 1)), I.upper j - I.lower j)

source

@[protected]

noncomputable def box_integral.box_additive_map.volume {ι : Type u_1} [fintype ι] {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] :

box_integral.box_additive_map ι (E →L[ℝ ] E) ⊤

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

Equations

box_integral.box_additive_map.volume = measure_theory.measure_space.volume.to_box_additive.to_smul

source

theorem box_integral.box_additive_map.volume_apply {ι : Type u_1} [fintype ι] {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] (I : box_integral.box ι) (x : E) :

⇑(⇑box_integral.box_additive_map.volume I) x = finset.univ.prod (λ (j : ι), I.upper j - I.lower j) • x