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 ℝ.
• ∫ᵛ x, f x ∂<•μ: the special case where f is an E-valued function and μ is a signed measure, with the pairing being the flip of scalar multiplication.
• ∫ᵛ x in s, f x ∂[B; μ]: the G-valued integral of an E-valued function f against the F-valued vector measure μ paired through B, on the set s.
• ∫ᵛ x in s, 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 ℝ.
• ∫ᵛ x in s, f x ∂<•μ: the special case where f is an E-valued function and μ is a signed measure, with the pairing being the flip of scalar multiplication.

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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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 (↑(μ.transpose B)) 1

theorem MeasureTheory.norm_cbmApplyMeasure_le {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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‖

@[simp]

theorem MeasureTheory.VectorMeasure.transpose_zero {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) : transpose 0 B = 0

theorem MeasureTheory.VectorMeasure.transpose_restrict {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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) : (μ.restrict s).transpose B = (μ.transpose B).restrict s

theorem MeasureTheory.VectorMeasure.transpose_map {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [MeasurableSpace Y] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) {φ : X → Y} : (μ.map φ).transpose B = (μ.transpose B).map φ

theorem MeasureTheory.VectorMeasure.transpose_add {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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 = μ.transpose B + ν.transpose B

theorem MeasureTheory.VectorMeasure.transpose_smul {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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 : ℝ) : (c • μ).transpose B = c • μ.transpose B

theorem MeasureTheory.VectorMeasure.transpose_dirac {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) (x : X) (v : F) : (dirac x v).transpose B = dirac x (B.flip v)

theorem MeasureTheory.VectorMeasure.variation_transpose_le {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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).variation ≤ ‖B‖₊ • μ.variation

theorem MeasureTheory.VectorMeasure.absolutelyContinuous_variation_transpose {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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).variation.AbsolutelyContinuous μ.variation

instance MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationContinuousLinearMapRealIdTranspose {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.transpose B).variation

theorem MeasureTheory.VectorMeasure.variation_transpose_eq_smul {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) [Nontrivial E] {C : NNReal} (hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = C * ‖x‖₊ * ‖y‖₊) : (μ.transpose B).variation = C • μ.variation

theorem MeasureTheory.VectorMeasure.variation_transpose_eq {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) [Nontrivial E] (hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖x‖₊ * ‖y‖₊) : (μ.transpose B).variation = μ.variation

@[simp]

theorem MeasureTheory.VectorMeasure.variation_transpose_lsmul {X : Type u_2} {F : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : VectorMeasure X F) : (μ.transpose (ContinuousLinearMap.lsmul ℝ ℝ)).variation = μ.variation

Control of the variation of the vector measure which appears in the integral of scalar functions with respect to a vector measure.

@[simp]

theorem MeasureTheory.VectorMeasure.variation_transpose_lsmul_flip {X : Type u_2} {E : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {μ : SignedMeasure X} : (transpose μ (ContinuousLinearMap.lsmul ℝ ℝ).flip).variation = variation μ

Control of the variation of the vector measure which appears in the integral of a vector function with respect to a signed measure.

@[reducible, inline]

abbrev MeasureTheory.VectorMeasure.Integrable {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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

@[reducible, inline]

abbrev MeasureTheory.VectorMeasure.IntegrableOn {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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) (s : Set X) : Prop

f : X → E is said to be integrable with respect to μ and B on s if it is integrable with respect to the vector measure μ.restrict s. When s is measurable, this is equivalent to integrability with respect to (μ.transpose B).variation.restrict s.

Equations

• μ.IntegrableOn f B s = (μ.restrict s).Integrable f B

noncomputable def MeasureTheory.VectorMeasure.integral {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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. Notation ∫ᵛ x, f x ∂[B; μ].

When μ is G-valued, to get the integral in G of a real-valued function, take B = ContinousLinearMap.lsmul ℝ ℝ. Notation ∫ᵛ x, f x ∂•μ. When μ is a signed measure, to get the integral in G of a G-valued function, take B = (ContinousLinearMap.lsmul ℝ ℝ).flip. Notation ∫ᵛ x, f x ∂<•μ.

Equations

• μ.integral f B = MeasureTheory.setToFun (μ.transpose B).variation ↑(μ.transpose B) ⋯ f

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. Notation ∫ᵛ x, f x ∂[B; μ].

When μ is G-valued, to get the integral in G of a real-valued function, take B = ContinousLinearMap.lsmul ℝ ℝ. Notation ∫ᵛ x, f x ∂•μ. When μ is a signed measure, to get the integral in G of a G-valued function, take B = (ContinousLinearMap.lsmul ℝ ℝ).flip. Notation ∫ᵛ x, f x ∂<•μ.

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.

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

The special case of the pairing integral where the pairing is just the flip of scalar multiplication by ℝ on F and f is F-valued and μ is a signed measure. The resulting integral is F-valued.

Equations

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

def MeasureTheory.VectorMeasure.«term∫ᵛ_In_,_∂[_;_]» : 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. Notation ∫ᵛ x, f x ∂[B; μ].

When μ is G-valued, to get the integral in G of a real-valued function, take B = ContinousLinearMap.lsmul ℝ ℝ. Notation ∫ᵛ x, f x ∂•μ. When μ is a signed measure, to get the integral in G of a G-valued function, take B = (ContinousLinearMap.lsmul ℝ ℝ).flip. Notation ∫ᵛ x, f x ∂<•μ.

Equations

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

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

The special case of the pairing integral in a set 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.

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

The special case of the pairing integral in a set where the pairing is just the flip of the scalar multiplication by ℝ on F and f is F-valued and μ is a signed measure. The resulting integral is F-valued.

Equations

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

theorem MeasureTheory.VectorMeasure.integral_eq_setToFun {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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; μ] = setToFun (μ.transpose B).variation ↑(μ.transpose B) ⋯ f

theorem MeasureTheory.VectorMeasure.integral_of_not_completeSpace {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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} (hG : ¬CompleteSpace G) : ∫ᵛ (x : X), f x ∂[B; μ] = 0

@[simp]

theorem MeasureTheory.VectorMeasure.transpose_zero_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) : μ.transpose 0 = 0

@[simp]

theorem MeasureTheory.VectorMeasure.transpose_add_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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 = μ.transpose B + ν.transpose B

@[simp]

theorem MeasureTheory.VectorMeasure.transpose_add_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B C : E →L[ℝ] F →L[ℝ] G) : μ.transpose (B + C) = μ.transpose B + μ.transpose C

@[simp]

theorem MeasureTheory.VectorMeasure.transpose_finsetSum_vectorMeasure {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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 : Finset ι) : (∑ i ∈ s, μ i).transpose B = ∑ i ∈ s, (μ i).transpose B

@[simp]

theorem MeasureTheory.VectorMeasure.transpose_finsetSum_cbm {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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 : Finset ι) : μ.transpose (∑ i ∈ s, B i) = ∑ i ∈ s, μ.transpose (B i)

@[simp]

theorem MeasureTheory.VectorMeasure.transpose_neg_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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 = -μ.transpose B

@[simp]

theorem MeasureTheory.VectorMeasure.transpose_neg_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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) = -μ.transpose B

@[simp]

theorem MeasureTheory.VectorMeasure.transpose_sub_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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 = μ.transpose B - ν.transpose B

@[simp]

theorem MeasureTheory.VectorMeasure.transpose_sub_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X F) (B C : E →L[ℝ] F →L[ℝ] G) : μ.transpose (B - C) = μ.transpose B - μ.transpose C

theorem MeasureTheory.VectorMeasure.integral_undef {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (h : ¬μ.Integrable f B) : ∫ᵛ (x : X), f x ∂[B; μ] = 0

@[simp]

theorem MeasureTheory.VectorMeasure.integral_zero {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} : ∫ᵛ (x : X), 0 ∂[B; μ] = 0

theorem MeasureTheory.VectorMeasure.integral_congr_ae {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (h : f =ᵐ[(μ.transpose B).variation] g) : ∫ᵛ (x : X), f x ∂[B; μ] = ∫ᵛ (x : X), g x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_eq_zero_of_ae {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hf : f =ᵐ[(μ.transpose B).variation] 0) : ∫ᵛ (x : X), f x ∂[B; μ] = 0

theorem MeasureTheory.VectorMeasure.Integrable.add {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hf : μ.Integrable f B) (hg : μ.Integrable g B) : μ.Integrable (f + g) B

theorem MeasureTheory.VectorMeasure.Integrable.fun_add {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hf : μ.Integrable f B) (hg : μ.Integrable g B) : μ.Integrable (fun (i : X) => f i + g i) B

Eta-expanded form of MeasureTheory.VectorMeasure.Integrable.add

theorem MeasureTheory.VectorMeasure.Integrable.neg {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hf : μ.Integrable f B) : μ.Integrable (-f) B

theorem MeasureTheory.VectorMeasure.Integrable.fun_neg {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hf : μ.Integrable f B) : μ.Integrable (fun (i : X) => -f i) B

Eta-expanded form of MeasureTheory.VectorMeasure.Integrable.neg

theorem MeasureTheory.VectorMeasure.Integrable.sub {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hf : μ.Integrable f B) (hg : μ.Integrable g B) : μ.Integrable (f - g) B

theorem MeasureTheory.VectorMeasure.Integrable.fun_sub {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hf : μ.Integrable f B) (hg : μ.Integrable g B) : μ.Integrable (fun (i : X) => f i - g i) B

Eta-expanded form of MeasureTheory.VectorMeasure.Integrable.sub

theorem MeasureTheory.VectorMeasure.Integrable.smul {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {𝕜 : Type u_7} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] (c : 𝕜) (hf : μ.Integrable f B) : μ.Integrable (c • f) B

theorem MeasureTheory.VectorMeasure.Integrable.fun_smul {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {𝕜 : Type u_7} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] (c : 𝕜) (hf : μ.Integrable f B) : μ.Integrable (fun (i : X) => c • f i) B

Eta-expanded form of MeasureTheory.VectorMeasure.Integrable.smul

theorem MeasureTheory.VectorMeasure.Integrable.finsetSum {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} (s : Finset ι) {f : ι → X → E} (hf : ∀ i ∈ s, μ.Integrable (f i) B) : μ.Integrable (∑ i ∈ s, f i) B

theorem MeasureTheory.VectorMeasure.Integrable.fun_finsetSum {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} (s : Finset ι) {f : ι → X → E} (hf : ∀ i ∈ s, μ.Integrable (f i) B) : μ.Integrable (fun (x : X) => ∑ i ∈ s, f i x) B

theorem MeasureTheory.VectorMeasure.integral_fun_add {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (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_finsetSum {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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 : Finset ι) {f : ι → X → E} (hf : ∀ i ∈ s, μ.Integrable (f i) B) : ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_fun_neg {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (f : X → E) (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) : ∫ᵛ (x : X), (-f) x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_fun_sub {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (f : X → E) (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (c : ℝ) : ∫ᵛ (x : X), (c • f) x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]

@[simp]

theorem MeasureTheory.VectorMeasure.integral_const {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] [IsFiniteMeasure (μ.transpose B).variation] (c : E) : ∫ᵛ (x : X), c ∂[B; μ] = (B c) (↑μ Set.univ)

@[simp]

theorem MeasureTheory.VectorMeasure.Integrable.zero_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} : VectorMeasure.Integrable 0 f B

theorem MeasureTheory.VectorMeasure.Integrable.add_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ ν : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hμ : μ.Integrable f B) (hν : ν.Integrable f B) : (μ + ν).Integrable f B

theorem MeasureTheory.VectorMeasure.Integrable.neg_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hμ : μ.Integrable f B) : (-μ).Integrable f B

theorem MeasureTheory.VectorMeasure.Integrable.sub_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ ν : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hμ : μ.Integrable f B) (hν : ν.Integrable f B) : (μ - ν).Integrable f B

theorem MeasureTheory.VectorMeasure.Integrable.smul_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hμ : μ.Integrable f B) (c : ℝ) : (c • μ).Integrable f B

theorem MeasureTheory.VectorMeasure.Integrable.finsetSum_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} {μ : ι → VectorMeasure X F} {s : Finset ι} (h : ∀ i ∈ s, (μ i).Integrable f B) : (∑ i ∈ s, μ i).Integrable f B

theorem MeasureTheory.VectorMeasure.Integrable.restrict {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hf : μ.Integrable f B) {s : Set X} : (μ.restrict s).Integrable f B

@[simp]

theorem MeasureTheory.VectorMeasure.integral_zero_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} : ∫ᵛ (x : X), f x ∂[B; 0] = 0

theorem MeasureTheory.VectorMeasure.integral_of_isEmpty {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} [IsEmpty X] : ∫ᵛ (x : X), f x ∂[B; μ] = 0

@[simp]

theorem MeasureTheory.VectorMeasure.integral_smul_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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) (c : ℝ) : ∫ᵛ (x : X), f x ∂[B; c • μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]

@[simp]

theorem MeasureTheory.VectorMeasure.integral_smul_nnreal_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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) (c : NNReal) : ∫ᵛ (x : X), f x ∂[B; c • μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_add_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ ν : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hμ : μ.Integrable f B) (hν : ν.Integrable f B) : ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]

theorem MeasureTheory.VectorMeasure.integral_finsetSum_vectorMeasure {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} {μ : ι → VectorMeasure X F} {s : Finset ι} (hf : ∀ i ∈ s, (μ i).Integrable f B) : ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]

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

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

@[simp]

theorem MeasureTheory.VectorMeasure.Integrable.zero_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} : μ.Integrable f 0

theorem MeasureTheory.VectorMeasure.Integrable.add_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B C : E →L[ℝ] F →L[ℝ] G} (hB : μ.Integrable f B) (hC : μ.Integrable f C) : μ.Integrable f (B + C)

theorem MeasureTheory.VectorMeasure.Integrable.neg_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hB : μ.Integrable f B) : μ.Integrable f (-B)

theorem MeasureTheory.VectorMeasure.Integrable.sub_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B C : E →L[ℝ] F →L[ℝ] G} (hB : μ.Integrable f B) (hC : μ.Integrable f C) : μ.Integrable f (B - C)

theorem MeasureTheory.VectorMeasure.Integrable.finsetSum_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {ι : Type u_7} {B : ι → E →L[ℝ] F →L[ℝ] G} {s : Finset ι} (h : ∀ i ∈ s, μ.Integrable f (B i)) : μ.Integrable f (∑ i ∈ s, B i)

@[simp]

theorem MeasureTheory.VectorMeasure.integral_zero_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (f : X → E) (μ : VectorMeasure X F) : ∫ᵛ (x : X), f x ∂[0; μ] = 0

theorem MeasureTheory.VectorMeasure.integral_add_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B C : E →L[ℝ] F →L[ℝ] G} (hB : μ.Integrable f B) (hC : μ.Integrable f C) : ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]

theorem MeasureTheory.VectorMeasure.integral_finsetSum_cbm {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : ι → E →L[ℝ] F →L[ℝ] G} {s : Finset ι} (hf : ∀ i ∈ s, μ.Integrable f (B i)) : ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]

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

theorem MeasureTheory.VectorMeasure.integral_sub_cbm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B C : E →L[ℝ] F →L[ℝ] G} (hB : μ.Integrable f B) (hC : μ.Integrable f C) : ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]

theorem MeasureTheory.VectorMeasure.Integrable.of_integral_ne_zero {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (h : ∫ᵛ (a : X), f a ∂[B; μ] ≠ 0) : μ.Integrable f B

theorem MeasureTheory.VectorMeasure.integral_non_aestronglyMeasurable {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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} (h : ¬AEStronglyMeasurable f (μ.transpose B).variation) : ∫ᵛ (a : X), f a ∂[B; μ] = 0

theorem MeasureTheory.VectorMeasure.integral_indicator₂ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_7} (f : β → X → E) (s : Set β) (b : β) : ∫ᵛ (y : X), s.indicator (fun (x : β) => f x y) b ∂[B; μ] = s.indicator (fun (x : β) => ∫ᵛ (y : X), f x y ∂[B; μ]) b

theorem MeasureTheory.VectorMeasure.norm_integral_le_lintegral_norm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} : ‖∫ᵛ (a : X), f a ∂[B; μ]‖ ≤ (∫⁻ (a : X), ENNReal.ofReal ‖f a‖ ∂(μ.transpose B).variation).toReal

theorem MeasureTheory.VectorMeasure.enorm_integral_le_lintegral_enorm {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} : ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.transpose B).variation

theorem MeasureTheory.VectorMeasure.dist_integral_le_lintegral_edist {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hf : μ.Integrable f B) (hg : μ.Integrable g B) : dist ∫ᵛ (a : X), f a ∂[B; μ] ∫ᵛ (a : X), g a ∂[B; μ] ≤ (∫⁻ (a : X), edist (f a) (g a) ∂(μ.transpose B).variation).toReal

theorem MeasureTheory.VectorMeasure.edist_integral_le_lintegral_edist {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (hf : μ.Integrable f B) (hg : μ.Integrable g B) : edist ∫ᵛ (a : X), f a ∂[B; μ] ∫ᵛ (a : X), g a ∂[B; μ] ≤ ∫⁻ (a : X), edist (f a) (g a) ∂(μ.transpose B).variation

theorem MeasureTheory.VectorMeasure.frequently_ae_ne_zero_of_integral_ne_zero {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (h : ∫ᵛ (a : X), f a ∂[B; μ] ≠ 0) : ∃ᵐ (a : X) ∂(μ.transpose B).variation, f a ≠ 0

theorem MeasureTheory.VectorMeasure.exists_ne_zero_of_integral_ne_zero {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (h : ∫ᵛ (a : X), f a ∂[B; μ] ≠ 0) : ∃ (a : X), f a ≠ 0

@[simp]

theorem MeasureTheory.VectorMeasure.integral_toSignedMeasure {X : Type u_2} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : Measure X} [IsFiniteMeasure μ] {f : X → G} : ∫ᵛ (x : X), f x ∂<•μ.toSignedMeasure = ∫ (x : X), f x ∂μ

@[simp]

theorem MeasureTheory.VectorMeasure.integral_dirac' {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} [MeasurableSpace X] [CompleteSpace G] {a : X} {v : F} (hfm : StronglyMeasurable f) : ∫ᵛ (x : X), f x ∂[B; dirac a v] = (B (f a)) v

@[simp]

theorem MeasureTheory.VectorMeasure.integral_dirac {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} [MeasurableSpace X] [MeasurableSingletonClass X] [CompleteSpace G] {a : X} {v : F} : ∫ᵛ (x : X), f x ∂[B; dirac a v] = (B (f a)) v

theorem MeasureTheory.VectorMeasure.integral_unique {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} [Unique X] [CompleteSpace G] : ∫ᵛ (x : X), f x ∂[B; μ] = (B (f default)) (↑μ Set.univ)

theorem MeasureTheory.VectorMeasure.tendsto_integral_of_L1 {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} (f : X → E) (hfi : AEStronglyMeasurable f (μ.transpose B).variation) {F✝ : ι → X → E} {l : Filter ι} (hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F✝ i) B) (hF : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : X), ‖F✝ i x - f x‖ₑ ∂(μ.transpose B).variation) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫ᵛ (x : X), F✝ i x ∂[B; μ]) l (nhds ∫ᵛ (x : X), f x ∂[B; μ])

If F i → f in L1, then ∫ᵛ x, F i x ∂[B; μ] → ∫ᵛ x, f x ∂[B; μ].

theorem MeasureTheory.VectorMeasure.tendsto_integral_of_L1' {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} (f : X → E) (hfi : AEStronglyMeasurable f (μ.transpose B).variation) {F✝ : ι → X → E} {l : Filter ι} (hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F✝ i) B) (hF : Filter.Tendsto (fun (i : ι) => eLpNorm (F✝ i - f) 1 (μ.transpose B).variation) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫ᵛ (x : X), F✝ i x ∂[B; μ]) l (nhds ∫ᵛ (x : X), f x ∂[B; μ])

If F i → f in L1, then ∫ᵛ x, F i x ∂[B; μ] → ∫ᵛ x, f x ∂[B; μ].

theorem MeasureTheory.VectorMeasure.continuousWithinAt_of_dominated {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {Y : Type u_7} [TopologicalSpace Y] [FirstCountableTopology Y] {F✝ : Y → X → E} {x₀ : Y} {bound : X → ℝ} {s : Set Y} (hF_meas : ∀ᶠ (x : Y) in nhdsWithin x₀ s, AEStronglyMeasurable (F✝ x) (μ.transpose B).variation) (h_bound : ∀ᶠ (x : Y) in nhdsWithin x₀ s, ∀ᵐ (a : X) ∂(μ.transpose B).variation, ‖F✝ x a‖ ≤ bound a) (bound_integrable : Integrable bound (μ.transpose B).variation) (h_cont : ∀ᵐ (a : X) ∂(μ.transpose B).variation, ContinuousWithinAt (fun (x : Y) => F✝ x a) s x₀) : ContinuousWithinAt (fun (x : Y) => ∫ᵛ (a : X), F✝ x a ∂[B; μ]) s x₀

theorem MeasureTheory.VectorMeasure.continuousAt_of_dominated {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {Y : Type u_7} [TopologicalSpace Y] [FirstCountableTopology Y] {F✝ : Y → X → E} {x₀ : Y} {bound : X → ℝ} (hF_meas : ∀ᶠ (x : Y) in nhds x₀, AEStronglyMeasurable (F✝ x) (μ.transpose B).variation) (h_bound : ∀ᶠ (x : Y) in nhds x₀, ∀ᵐ (a : X) ∂(μ.transpose B).variation, ‖F✝ x a‖ ≤ bound a) (bound_integrable : Integrable bound (μ.transpose B).variation) (h_cont : ∀ᵐ (a : X) ∂(μ.transpose B).variation, ContinuousAt (fun (x : Y) => F✝ x a) x₀) : ContinuousAt (fun (x : Y) => ∫ᵛ (a : X), F✝ x a ∂[B; μ]) x₀

theorem MeasureTheory.VectorMeasure.continuousOn_of_dominated {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {Y : Type u_7} [TopologicalSpace Y] [FirstCountableTopology Y] {F✝ : Y → X → E} {bound : X → ℝ} {s : Set Y} (hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F✝ x) (μ.transpose B).variation) (h_bound : ∀ x ∈ s, ∀ᵐ (a : X) ∂(μ.transpose B).variation, ‖F✝ x a‖ ≤ bound a) (bound_integrable : Integrable bound (μ.transpose B).variation) (h_cont : ∀ᵐ (a : X) ∂(μ.transpose B).variation, ContinuousOn (fun (x : Y) => F✝ x a) s) : ContinuousOn (fun (x : Y) => ∫ᵛ (a : X), F✝ x a ∂[B; μ]) s

theorem MeasureTheory.VectorMeasure.continuous_of_dominated {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {Y : Type u_7} [TopologicalSpace Y] [FirstCountableTopology Y] {F✝ : Y → X → E} {bound : X → ℝ} (hF_meas : ∀ (x : Y), AEStronglyMeasurable (F✝ x) (μ.transpose B).variation) (h_bound : ∀ (x : Y), ∀ᵐ (a : X) ∂(μ.transpose B).variation, ‖F✝ x a‖ ≤ bound a) (bound_integrable : Integrable bound (μ.transpose B).variation) (h_cont : ∀ᵐ (a : X) ∂(μ.transpose B).variation, Continuous fun (x : Y) => F✝ x a) : Continuous fun (x : Y) => ∫ᵛ (a : X), F✝ x a ∂[B; μ]

theorem MeasureTheory.VectorMeasure.norm_integral_le_of_norm_le_const {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} [IsFiniteMeasure (μ.transpose B).variation] {C : ℝ} (h : ∀ᵐ (x : X) ∂(μ.transpose B).variation, ‖f x‖ ≤ C) : ‖∫ᵛ (x : X), f x ∂[B; μ]‖ ≤ C * (μ.transpose B).variation.real Set.univ

theorem MeasureTheory.VectorMeasure.enorm_integral_le_of_enorm_le_const {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {C : ENNReal} (h : ∀ᵐ (x : X) ∂(μ.transpose B).variation, ‖f x‖ₑ ≤ C) : ‖∫ᵛ (x : X), f x ∂[B; μ]‖ₑ ≤ C * (μ.transpose B).variation Set.univ

theorem MeasureTheory.VectorMeasure.nndist_integral_add_vectorMeasure_le_lintegral {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → E} {μ ν : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (h₁ : μ.Integrable f B) (h₂ : ν.Integrable f B) : ↑(nndist ∫ᵛ (x : X), f x ∂[B; μ] ∫ᵛ (x : X), f x ∂[B; μ + ν]) ≤ ∫⁻ (x : X), ‖f x‖ₑ ∂(ν.transpose B).variation

theorem MeasureTheory.VectorMeasure.variation_transpose_map_le {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_8} [MeasurableSpace β] {φ : X → β} : ((μ.map φ).transpose B).variation ≤ Measure.map φ (μ.transpose B).variation

theorem MeasureTheory.VectorMeasure.Integrable.map {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_9} [MeasurableSpace β] {φ : X → β} {f : β → E} (hfm : AEStronglyMeasurable f (Measure.map φ (μ.transpose B).variation)) (h : μ.Integrable (f ∘ φ) B) : (μ.map φ).Integrable f B

theorem MeasureTheory.VectorMeasure.integral_map {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_9} [MeasurableSpace β] {φ : X → β} (hφ : Measurable φ) {f : β → E} (hfm : AEStronglyMeasurable f (Measure.map φ (μ.transpose B).variation)) (hfi' : μ.Integrable (f ∘ φ) B) : ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]

theorem MeasurableEmbedding.variation_transpose_map {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_8} [MeasurableSpace β] {φ : X → β} (hφ : MeasurableEmbedding φ) : ((μ.map φ).transpose B).variation = MeasureTheory.Measure.map φ (μ.transpose B).variation

theorem MeasurableEmbedding.integrable_map_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_8} [MeasurableSpace β] {φ : X → β} (hφ : MeasurableEmbedding φ) {f : β → E} : (μ.map φ).Integrable f B ↔ μ.Integrable (f ∘ φ) B

theorem MeasurableEmbedding.integral_map_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_8} [MeasurableSpace β] {φ : X → β} (hφ : MeasurableEmbedding φ) {f : β → E} : ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]

theorem Topology.IsClosedEmbedding.integral_map_vectorMeasure {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_8} [MeasurableSpace β] {φ : X → β} [TopologicalSpace X] [BorelSpace X] [TopologicalSpace β] [BorelSpace β] (hφ : IsClosedEmbedding φ) {f : β → E} : ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]

theorem MeasureTheory.VectorMeasure.integral_map_equiv {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_9} [MeasurableSpace β] (e : X ≃ᵐ β) (f : β → E) : ∫ᵛ (y : β), f y ∂[B; μ.map ⇑e] = ∫ᵛ (x : X), f (e x) ∂[B; μ]

theorem MeasureTheory.VectorMeasure.tendsto_integral_of_dominated_convergence {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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} {f : X → E} (bound : X → ℝ) (F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F✝ n) (μ.transpose B).variation) (bound_integrable : Integrable bound (μ.transpose B).variation) (h_bound : ∀ (n : ℕ), ∀ᵐ (a : X) ∂(μ.transpose B).variation, ‖F✝ n a‖ ≤ bound a) (h_lim : ∀ᵐ (a : X) ∂(μ.transpose B).variation, Filter.Tendsto (fun (n : ℕ) => F✝ n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun (n : ℕ) => ∫ᵛ (a : X), F✝ n a ∂[B; μ]) Filter.atTop (nhds ∫ᵛ (a : X), f a ∂[B; μ])

Lebesgue dominated convergence theorem provides sufficient conditions under which almost everywhere convergence of a sequence of functions implies the convergence of their integrals. We could weaken the condition bound_integrable to require HasFiniteIntegral bound (μ.transpose B).variation instead (i.e. not requiring that bound is measurable), but in all applications proving integrability is easier.

theorem MeasureTheory.VectorMeasure.tendsto_integral_filter_of_dominated_convergence {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {l : Filter ι} [l.IsCountablyGenerated] {F✝ : ι → X → E} {f : X → E} (bound : X → ℝ) (hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F✝ n) (μ.transpose B).variation) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : X) ∂(μ.transpose B).variation, ‖F✝ n a‖ ≤ bound a) (bound_integrable : Integrable bound (μ.transpose B).variation) (h_lim : ∀ᵐ (a : X) ∂(μ.transpose B).variation, Filter.Tendsto (fun (n : ι) => F✝ n a) l (nhds (f a))) : Filter.Tendsto (fun (n : ι) => ∫ᵛ (a : X), F✝ n a ∂[B; μ]) l (nhds ∫ᵛ (a : X), f a ∂[B; μ])

Lebesgue dominated convergence theorem for filters with a countable basis

theorem MeasureTheory.VectorMeasure.hasSum_integral_of_dominated_convergence {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} [Countable ι] {F✝ : ι → X → E} {f : X → E} (bound : ι → X → ℝ) (hF_meas : ∀ (n : ι), AEStronglyMeasurable (F✝ n) (μ.transpose B).variation) (h_bound : ∀ (n : ι), ∀ᵐ (a : X) ∂(μ.transpose B).variation, ‖F✝ n a‖ ≤ bound n a) (bound_summable : ∀ᵐ (a : X) ∂(μ.transpose B).variation, Summable fun (n : ι) => bound n a) (bound_integrable : Integrable (fun (a : X) => ∑' (n : ι), bound n a) (μ.transpose B).variation) (h_lim : ∀ᵐ (a : X) ∂(μ.transpose B).variation, HasSum (fun (n : ι) => F✝ n a) (f a)) : HasSum (fun (n : ι) => ∫ᵛ (a : X), F✝ n a ∂[B; μ]) ∫ᵛ (a : X), f a ∂[B; μ]

Lebesgue dominated convergence theorem for series.

theorem MeasureTheory.VectorMeasure.integral_tsum {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace E] [Countable ι] {f : ι → X → E} (hf : ∀ (i : ι), AEStronglyMeasurable (f i) (μ.transpose B).variation) (hf' : ∑' (i : ι), ∫⁻ (a : X), ‖f i a‖ₑ ∂(μ.transpose B).variation ≠ ⊤) : ∫ᵛ (a : X), ∑' (i : ι), f i a ∂[B; μ] = ∑' (i : ι), ∫ᵛ (a : X), f i a ∂[B; μ]

theorem MeasureTheory.VectorMeasure.tendsto_integral_filter_of_norm_le_const {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {l : Filter ι} [l.IsCountablyGenerated] {F✝ : ι → X → E} [IsFiniteMeasure (μ.transpose B).variation] {f : X → E} (h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F✝ n) (μ.transpose B).variation) (h_bound : ∃ (C : ℝ), ∀ᶠ (n : ι) in l, ∀ᵐ (a : X) ∂(μ.transpose B).variation, ‖F✝ n a‖ ≤ C) (h_lim : ∀ᵐ (a : X) ∂(μ.transpose B).variation, Filter.Tendsto (fun (n : ι) => F✝ n a) l (nhds (f a))) : Filter.Tendsto (fun (n : ι) => ∫ᵛ (a : X), F✝ n a ∂[B; μ]) l (nhds ∫ᵛ (a : X), f a ∂[B; μ])

Corollary of the Lebesgue dominated convergence theorem: If a sequence of functions F n is (eventually) uniformly bounded by a constant and converges (eventually) pointwise to a function f, then the integrals of F n with respect to a vector measure μ with finite variation converge to the integral of f.