Integral of vector-valued function against vector measure

We extend the definition of the Bochner integral (of vector-valued function against ℝ≥0∞-valued measure) to vector measures through a bilinear pairing. Let E, F be normed vector spaces, and G be a Banach space (complete normed vector space). We fix a continuous linear pairing B : E →L[ℝ] F →L[ℝ] G and an F-valued vector measure μ on a measurable space X. For an integrable function f : X → E with respect to the total variation of the vector measure on X informally written μ ∘ B.flip, we define the G-valued integral, which is informally written ∫ B (f x) ∂μ x.

Such integral is defined through the general setting setToFun which sends a set function to the integral of integrable functions, see the file Mathlib/MeasureTheory/Integral/SetToL1.lean.

Main definitions

The integral against vector measures is defined through the extension process described in the file Mathlib/MeasureTheory/Integral/SetToL1.lean, which follows these steps:

1. Define the integral of the indicator of a set. This is cbmApplyMeasure B μ s x = B x (μ s). cbmApplyMeasure B μ is shown to be linear in the value x and DominatedFinMeasAdditive (defined in the file Mathlib/MeasureTheory/Integral/SetToL1.lean) with respect to the set s.

2. Define the integral on integrable functions f as setToFun (...) f.

Notations

• ∫ᵛ x, f x ∂[B; μ]: the G-valued integral of an E-valued function f against the F-valued vector measure μ paired through B.
• ∫ᵛ x, f x ∂•μ: the special case where f is a real-valued function and μ is an F-valued vector measure, with the pairing being the scalar multiplication by ℝ.

Note

Let μ be a vector measure and B be a continuous linear pairing. We often consider integrable functions with respect to the total variation of μ.transpose B = μ.mapRange B.flip.toAddMonoidHom B.flip.continuous, which is the reference measure for the pairing integral.

When f is not integrable with respect to (μ.transpose B).variation, the value of μ.integral B f is set to 0. This is an analogous convention to the Bochner integral. However, there are cases where a natural definition of the integral as an unconditional sum exists, but f is not integrable in this sense: Let μ be the L∞(ℕ)-valued measure on ℕ defined by extending {n} ↦ (0,0,..., 1/(n+1),0,0,...) and B be the trivial coupling (the scalar multiplication by ℝ). The total variation is ∑ n, 1/(n+1) = ∞, but the sum of (0,...,0,1/n,0,...) in L∞(ℕ) is unconditionally convergent.

noncomputable def MeasureTheory.VectorMeasure.transpose {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) : VectorMeasure X (E →L[ℝ] G)

The composition of the vector measure with the linear pairing, giving the reference vector measure.

Equations

• μ.transpose B = μ.mapRange (↑B.flip).toAddMonoidHom ⋯

noncomputable def MeasureTheory.cbmApplyMeasure {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (s : Set X) : E →L[ℝ] G

Given a set s, return the continuous linear map fun x : E ↦ B x (μ s) (actually defined using transpose through mapRange), where the B is a G-valued bilinear form on E × F and μ is an F-valued vector measure. The extension of that set function through setToFun gives the pairing integral of E-valued integrable functions.

Equations

• MeasureTheory.cbmApplyMeasure μ B s = { toFun := fun (x : E) => (↑(μ.transpose B) s) x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem MeasureTheory.transpose_eq_cbmApplyMeasure {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) : ↑(μ.transpose B) = cbmApplyMeasure μ B

@[simp]

theorem MeasureTheory.cbmApplyMeasure_apply {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (s : Set X) (x : E) : (cbmApplyMeasure μ B s) x = (B x) (↑μ s)

theorem MeasureTheory.cbmApplyMeasure_union {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) {s t : Set X} (hs : MeasurableSet s) (ht : MeasurableSet t) (hdisj : Disjoint s t) : cbmApplyMeasure μ B (s ∪ t) = cbmApplyMeasure μ B s + cbmApplyMeasure μ B t

theorem MeasureTheory.dominatedFinMeasAdditive_cbmApplyMeasure {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) : DominatedFinMeasAdditive (μ.transpose B).variation (cbmApplyMeasure μ B) 1

theorem MeasureTheory.norm_cbmApplyMeasure_le {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (s : Set X) : ‖cbmApplyMeasure μ B s‖ ≤ ‖B‖ * ‖↑μ s‖

@[reducible, inline]

abbrev MeasureTheory.VectorMeasure.Integrable {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (f : X → E) (B : E →L[ℝ] F →L[ℝ] G) : Prop

f : X → E is said to be integrable with respect to μ and B if it is integrable with respect to (μ.transpose B).variation.

Equations

• μ.Integrable f B = MeasureTheory.Integrable f (μ.transpose B).variation

noncomputable def MeasureTheory.VectorMeasure.integral {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (f : X → E) (B : E →L[ℝ] F →L[ℝ] G) : G

The G-valued integral of E-valued function and the F-valued vector measure μ with linear paring B : E →L[ℝ] F →L[ℝ] G . This is set to be 0 if G is not complete or if f is not integrable with respect to (μ.transpose B).variation.

Equations

• μ.integral f B = if x : CompleteSpace G then MeasureTheory.setToFun (μ.transpose B).variation ↑(μ.transpose B) ⋯ f else 0

def MeasureTheory.VectorMeasure.«term∫ᵛ_,_∂[_;_]» : Lean.ParserDescr

The G-valued integral of E-valued function and the F-valued vector measure μ with linear paring B : E →L[ℝ] F →L[ℝ] G . This is set to be 0 if G is not complete or if f is not integrable with respect to (μ.transpose B).variation.

Equations

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

def MeasureTheory.VectorMeasure.«term∫ᵛ_,_∂•_» : Lean.ParserDescr

The special case of the pairing integral where the pairing is just the scalar multiplication by ℝ on F and f is real-valued. The resulting integral is F-valued.

Equations

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

theorem MeasureTheory.VectorMeasure.integral_fun_add {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {f g : X → E} (hf : μ.Integrable f B) (hg : μ.Integrable g B) : ∫ᵛ (x : X), f x + g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_add {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {f g : X → E} (hf : μ.Integrable f B) (hg : μ.Integrable g B) : ∫ᵛ (x : X), (f + g) x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_fun_neg {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (f : X → E) : ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_neg {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (f : X → E) : ∫ᵛ (x : X), (-f) x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_fun_sub {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {f g : X → E} (hf : μ.Integrable f B) (hg : μ.Integrable g B) : ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_sub {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {f g : X → E} (hf : μ.Integrable f B) (hg : μ.Integrable g B) : ∫ᵛ (x : X), (f - g) x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_fun_smul {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (c : ℝ) (f : X → E) : ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_smul {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (c : ℝ) (f : X → E) : ∫ᵛ (x : X), (c • f) x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]