Integration by parts for vector measures associated to bounded variation functions

Consider two bounded variation functions f and g. We give several versions of the integration by parts formula ∫_a^b f dg = f b * g b - f a * g a - ∫_a^b g df. Note that the formula as written is wrong in case of discontinuities : one should use left limits and right limits, and pay attention as to whether a and b are included in the integrals. Therefore, we give 4 versions, on Icc and Ioc and Ico and Ioo. They all follow from a formula on a general set s, where the boundary contribution is the integral on s of the vector measure associated to the bounded variation function fg.

Main results

We denote by f⁻ x the left limit of f at x, and by f⁺ x its right limit.

• vectorMeasure_bilinear_comp_eq states that d(fg) = g⁺ df + f⁻ dg, for a general pairing function
• setIntegral_Icc_leftLim_vectorMeasure_eq_sub gives the equality ∫_[a, b] f⁻ dg = f⁺ b * g⁺ b - f⁻ a * g⁻ a - ∫_[a, b] g⁺ df, for a general pairing function.
• There are also versions for Ioc and Ico and Ioo.
• There are also versions where the pairing is scalar multiplication. For instance, the Icc version is setIntegral_Icc_leftLim_smul_vectorMeasure_eq_sub.
• There are versions of all the previous statements using f⁺ and g⁻ instead. The names are the same, modulo the replacement of leftLim with rightLim.

theorem MeasureTheory.VectorMeasure.ext_of_Icc {α : Type u_1} {E : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] (μ ν : VectorMeasure α E) (hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Set.Icc a b) = ν (Set.Icc a b)) : μ = ν

Two vector measures which agree on closed intervals are equal.

@[simp]

theorem BoundedVariationOn.rightLim_bilinear_comp {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] {α : Type u_6} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : α → E} {g : α → F} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (B : E →L[ℝ] F →L[ℝ] G) : (Function.rightLim fun (x : α) => (B (f x)) (g x)) = fun (x : α) => (B (Function.rightLim f x)) (Function.rightLim g x)

@[simp]

theorem BoundedVariationOn.leftLim_bilinear_comp {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] {α : Type u_6} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : α → E} {g : α → F} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (B : E →L[ℝ] F →L[ℝ] G) : (Function.leftLim fun (x : α) => (B (f x)) (g x)) = fun (x : α) => (B (Function.leftLim f x)) (Function.leftLim g x)

theorem BoundedVariationOn.setIntegral_Icc_rightLim_sub_leftLim_eq {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {a b : α} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) : ∫ᵛ (x : α) in Set.Icc a b, Function.rightLim g x - Function.leftLim g a ∂[B.flip; hf.vectorMeasure] = ∫ᵛ (y : α) in Set.Icc a b, Function.rightLim f b - Function.leftLim f y ∂[B; hg.vectorMeasure]

theorem BoundedVariationOn.vectorMeasure_bilinear_comp_eq {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) : ⋯.vectorMeasure = hf.vectorMeasure.withDensity (Function.rightLim g) B.flip + hg.vectorMeasure.withDensity (Function.leftLim f) B

Given bounded variation functions, the measure associated to their product is given by d (f * g) = f⁻ dg + g⁺ df. Version for a general pairing instead of multiplication. This is the most general version of the integration by parts formula for vector measures.

theorem BoundedVariationOn.vectorMeasure_bilinear_comp_eq' {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) : ⋯.vectorMeasure = hf.vectorMeasure.withDensity (Function.leftLim g) B.flip + hg.vectorMeasure.withDensity (Function.rightLim f) B

Given bounded variation functions, the measure associated to their product is given by d (f * g) = f⁺ dg + g⁻ df. Version for a general pairing instead of multiplication. This is the most general version of the integration by parts formula for vector measures.

theorem BoundedVariationOn.setIntegral_leftLim_vectorMeasure_eq_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {s : Set α} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) : ∫ᵛ (x : α) in s, Function.leftLim f x ∂[B; hg.vectorMeasure] = ⋯.vectorMeasure s - ∫ᵛ (x : α) in s, Function.rightLim g x ∂[B.flip; hf.vectorMeasure]

Integration by parts for Stieltjes vector measure, between f.leftLim dg and g.rightLim df. Version with a general pairing function B, and over a general integration set s.

theorem BoundedVariationOn.setIntegral_rightLim_vectorMeasure_eq_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {s : Set α} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) : ∫ᵛ (x : α) in s, Function.rightLim f x ∂[B; hg.vectorMeasure] = ⋯.vectorMeasure s - ∫ᵛ (x : α) in s, Function.leftLim g x ∂[B.flip; hf.vectorMeasure]

Integration by parts for Stieltjes vector measure, between f.rightLim dg and g.leftLim df. Version with a general pairing function B, and over a general integration set s.

theorem BoundedVariationOn.setIntegral_Icc_leftLim_vectorMeasure_eq_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {a b : α} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Icc a b, Function.leftLim f x ∂[B; hg.vectorMeasure] = (B (Function.rightLim f b)) (Function.rightLim g b) - (B (Function.leftLim f a)) (Function.leftLim g a) - ∫ᵛ (x : α) in Set.Icc a b, Function.rightLim g x ∂[B.flip; hf.vectorMeasure]

Integration by parts for Stieltjes vector measure, between f.leftLim dg and g.rightLim df. Version with a general pairing function B, over an interval [a, b].

theorem BoundedVariationOn.setIntegral_Icc_rightLim_vectorMeasure_eq_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {a b : α} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Icc a b, Function.rightLim f x ∂[B; hg.vectorMeasure] = (B (Function.rightLim f b)) (Function.rightLim g b) - (B (Function.leftLim f a)) (Function.leftLim g a) - ∫ᵛ (x : α) in Set.Icc a b, Function.leftLim g x ∂[B.flip; hf.vectorMeasure]

Integration by parts for Stieltjes vector measure, between f.rightLim dg and g.leftLim df. Version with a general pairing function B, over an interval [a, b].

theorem BoundedVariationOn.setIntegral_Ioc_leftLim_vectorMeasure_eq_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {a b : α} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Ioc a b, Function.leftLim f x ∂[B; hg.vectorMeasure] = (B (Function.rightLim f b)) (Function.rightLim g b) - (B (Function.rightLim f a)) (Function.rightLim g a) - ∫ᵛ (x : α) in Set.Ioc a b, Function.rightLim g x ∂[B.flip; hf.vectorMeasure]

Integration by parts for Stieltjes vector measure, between f.leftLim dg and g.rightLim df. Version with a general pairing function B, over an interval (a, b].

theorem BoundedVariationOn.setIntegral_Ioc_rightLim_vectorMeasure_eq_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {a b : α} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Ioc a b, Function.rightLim f x ∂[B; hg.vectorMeasure] = (B (Function.rightLim f b)) (Function.rightLim g b) - (B (Function.rightLim f a)) (Function.rightLim g a) - ∫ᵛ (x : α) in Set.Ioc a b, Function.leftLim g x ∂[B.flip; hf.vectorMeasure]

Integration by parts for Stieltjes vector measure, between f.rightLim dg and g.leftLim df. Version with a general pairing function B, over an interval (a, b].

theorem BoundedVariationOn.setIntegral_Ico_leftLim_vectorMeasure_eq_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {a b : α} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Ico a b, Function.leftLim f x ∂[B; hg.vectorMeasure] = (B (Function.leftLim f b)) (Function.leftLim g b) - (B (Function.leftLim f a)) (Function.leftLim g a) - ∫ᵛ (x : α) in Set.Ico a b, Function.rightLim g x ∂[B.flip; hf.vectorMeasure]

Integration by parts for Stieltjes vector measure, between f.leftLim dg and g.rightLim df. Version with a general pairing function B, over an interval [a, b).

theorem BoundedVariationOn.setIntegral_Ico_rightLim_vectorMeasure_eq_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {a b : α} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Ico a b, Function.rightLim f x ∂[B; hg.vectorMeasure] = (B (Function.leftLim f b)) (Function.leftLim g b) - (B (Function.leftLim f a)) (Function.leftLim g a) - ∫ᵛ (x : α) in Set.Ico a b, Function.leftLim g x ∂[B.flip; hf.vectorMeasure]

Integration by parts for Stieltjes vector measure, between f.rightLim dg and g.leftLim df. Version with a general pairing function B, over an interval [a, b).

theorem BoundedVariationOn.setIntegral_Ioo_leftLim_vectorMeasure_eq_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {a b : α} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a < b) : ∫ᵛ (x : α) in Set.Ioo a b, Function.leftLim f x ∂[B; hg.vectorMeasure] = (B (Function.leftLim f b)) (Function.leftLim g b) - (B (Function.rightLim f a)) (Function.rightLim g a) - ∫ᵛ (x : α) in Set.Ioo a b, Function.rightLim g x ∂[B.flip; hf.vectorMeasure]

Integration by parts for Stieltjes vector measure, between f.leftLim dg and g.rightLim df. Version with a general pairing function B, over an interval (a, b).

theorem BoundedVariationOn.setIntegral_Ioo_rightLim_vectorMeasure_eq_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [CompleteSpace E] [NormedSpace ℝ F] [CompleteSpace F] [NormedSpace ℝ G] [DenselyOrdered α] [CompactIccSpace α] {f : α → E} {g : α → F} {B : E →L[ℝ] F →L[ℝ] G} {a b : α} [CompleteSpace G] (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a < b) : ∫ᵛ (x : α) in Set.Ioo a b, Function.rightLim f x ∂[B; hg.vectorMeasure] = (B (Function.leftLim f b)) (Function.leftLim g b) - (B (Function.rightLim f a)) (Function.rightLim g a) - ∫ᵛ (x : α) in Set.Ioo a b, Function.leftLim g x ∂[B.flip; hf.vectorMeasure]

Integration by parts for Stieltjes vector measure, between f.rightLim dg and g.leftLim df. Version with a general pairing function B, over an interval (a, b).

theorem BoundedVariationOn.setIntegral_Icc_leftLim_smul_vectorMeasure_eq_sub {α : Type u_1} {F : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [DenselyOrdered α] [CompactIccSpace α] {g : α → F} {a b : α} {f : α → ℝ} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Icc a b, Function.leftLim f x ∂•hg.vectorMeasure = Function.rightLim f b • Function.rightLim g b - Function.leftLim f a • Function.leftLim g a - ∫ᵛ (x : α) in Set.Icc a b, Function.rightLim g x ∂<•hf.vectorMeasure

Integration by parts for Stieltjes vector measure, between f.leftLim dg and g.rightLim df. Version for scalar multiplication, over an interval [a, b].

theorem BoundedVariationOn.setIntegral_Icc_rightLim_smul_vectorMeasure_eq_sub {α : Type u_1} {F : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [DenselyOrdered α] [CompactIccSpace α] {g : α → F} {a b : α} {f : α → ℝ} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Icc a b, Function.rightLim f x ∂•hg.vectorMeasure = Function.rightLim f b • Function.rightLim g b - Function.leftLim f a • Function.leftLim g a - ∫ᵛ (x : α) in Set.Icc a b, Function.leftLim g x ∂<•hf.vectorMeasure

Integration by parts for Stieltjes vector measure, between f.rightLim dg and g.leftLim df. Version for scalar multiplication, over an interval [a, b].

theorem BoundedVariationOn.setIntegral_Ioc_leftLim_smul_vectorMeasure_eq_sub {α : Type u_1} {F : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [DenselyOrdered α] [CompactIccSpace α] {g : α → F} {a b : α} {f : α → ℝ} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Ioc a b, Function.leftLim f x ∂•hg.vectorMeasure = Function.rightLim f b • Function.rightLim g b - Function.rightLim f a • Function.rightLim g a - ∫ᵛ (x : α) in Set.Ioc a b, Function.rightLim g x ∂<•hf.vectorMeasure

Integration by parts for Stieltjes vector measure, between f.leftLim dg and g.rightLim df. Version for scalar multiplication, over an interval (a, b].

theorem BoundedVariationOn.setIntegral_Ioc_rightLim_smul_vectorMeasure_eq_sub {α : Type u_1} {F : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [DenselyOrdered α] [CompactIccSpace α] {g : α → F} {a b : α} {f : α → ℝ} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Ioc a b, Function.rightLim f x ∂•hg.vectorMeasure = Function.rightLim f b • Function.rightLim g b - Function.rightLim f a • Function.rightLim g a - ∫ᵛ (x : α) in Set.Ioc a b, Function.leftLim g x ∂<•hf.vectorMeasure

Integration by parts for Stieltjes vector measure, between f.rightLim dg and g.leftLim df. Version for scalar multiplication, over an interval (a, b].

theorem BoundedVariationOn.setIntegral_Ico_leftLim_smul_vectorMeasure_eq_sub {α : Type u_1} {F : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [DenselyOrdered α] [CompactIccSpace α] {g : α → F} {a b : α} {f : α → ℝ} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Ico a b, Function.leftLim f x ∂•hg.vectorMeasure = Function.leftLim f b • Function.leftLim g b - Function.leftLim f a • Function.leftLim g a - ∫ᵛ (x : α) in Set.Ico a b, Function.rightLim g x ∂<•hf.vectorMeasure

Integration by parts for Stieltjes vector measure, between f.leftLim dg and g.rightLim df. Version for scalar multiplication, over an interval [a, b).

theorem BoundedVariationOn.setIntegral_Ico_rightLim_smul_vectorMeasure_eq_sub {α : Type u_1} {F : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [DenselyOrdered α] [CompactIccSpace α] {g : α → F} {a b : α} {f : α → ℝ} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a ≤ b) : ∫ᵛ (x : α) in Set.Ico a b, Function.rightLim f x ∂•hg.vectorMeasure = Function.leftLim f b • Function.leftLim g b - Function.leftLim f a • Function.leftLim g a - ∫ᵛ (x : α) in Set.Ico a b, Function.leftLim g x ∂<•hf.vectorMeasure

Integration by parts for Stieltjes vector measure, between f.rightLim dg and g.leftLim df. Version for scalar multiplication, over an interval [a, b).

theorem BoundedVariationOn.setIntegral_Ioo_leftLim_smul_vectorMeasure_eq_sub {α : Type u_1} {F : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [DenselyOrdered α] [CompactIccSpace α] {g : α → F} {a b : α} {f : α → ℝ} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a < b) : ∫ᵛ (x : α) in Set.Ioo a b, Function.leftLim f x ∂•hg.vectorMeasure = Function.leftLim f b • Function.leftLim g b - Function.rightLim f a • Function.rightLim g a - ∫ᵛ (x : α) in Set.Ioo a b, Function.rightLim g x ∂<•hf.vectorMeasure

Integration by parts for Stieltjes vector measure, between f.leftLim dg and g.rightLim df. Version for scalar multiplication, over an interval (a, b).

theorem BoundedVariationOn.setIntegral_Ioo_rightLim_smul_vectorMeasure_eq_sub {α : Type u_1} {F : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [DenselyOrdered α] [CompactIccSpace α] {g : α → F} {a b : α} {f : α → ℝ} (hf : BoundedVariationOn f Set.univ) (hg : BoundedVariationOn g Set.univ) (hab : a < b) : ∫ᵛ (x : α) in Set.Ioo a b, Function.rightLim f x ∂•hg.vectorMeasure = Function.leftLim f b • Function.leftLim g b - Function.rightLim f a • Function.rightLim g a - ∫ᵛ (x : α) in Set.Ioo a b, Function.leftLim g x ∂<•hf.vectorMeasure

Integration by parts for Stieltjes vector measure, between f.rightLim dg and g.leftLim df. Version for scalar multiplication, over an interval (a, b).