Vector measure with density with respect to a vector measure

Given a vector measure μ, a function f and a pairing B, we define the vector measure with density f and pairing B, denoted μ.withDensity f B. It associates to a measurable set the mass ∫ᵛ x in s, f x ∂[B; μ].

This file implements the basic property of this notion. Notably, we show in variation_withDensity that the variation of the vector measure μ.withDensity f B is the positive measure with density ‖f‖ with respect to the positive measure μ.variation.

noncomputable def MeasureTheory.VectorMeasure.withDensity {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) : VectorMeasure X G

The vector measure with density f with respect to a vector measure μ, associating to a measurable set the mass ∫ᵛ x in s, f x ∂[B; μ]. If f is not integrable, we use the junk value 0.

Equations

• μ.withDensity f B = if h : μ.Integrable f then { measureOf' := fun (s : Set X) => ∫ᵛ (x : X) in s, f x ∂[B; μ], empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ } else 0

theorem MeasureTheory.VectorMeasure.withDensity_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} {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} {s : Set X} (hf : μ.Integrable f) : (μ.withDensity f B) s = ∫ᵛ (x : X) in s, f x ∂[B; μ]

theorem MeasureTheory.VectorMeasure.withDensity_apply_univ {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} : (μ.withDensity f B) Set.univ = ∫ᵛ (x : X), f x ∂[B; μ]

@[simp]

theorem MeasureTheory.VectorMeasure.withDensity_zero_vectorMeasure {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] {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} : withDensity 0 f B = 0

@[simp]

theorem MeasureTheory.VectorMeasure.withDensity_zero {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} : μ.withDensity 0 B = 0

@[simp]

theorem MeasureTheory.VectorMeasure.withDensity_fun_zero {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} : μ.withDensity (fun (x : X) => 0) B = 0

Eta-expanded form of MeasureTheory.VectorMeasure.withDensity_zero

theorem MeasureTheory.VectorMeasure.withDensity_congr {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 g : X → E} {B : E →L[ℝ] F →L[ℝ] G} (h : f =ᵐ[μ.variation] g) : μ.withDensity f B = μ.withDensity g B

theorem MeasureTheory.VectorMeasure.restrict_withDensity {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} {s : Set X} (hf : μ.Integrable f) : (μ.withDensity f B).restrict s = (μ.restrict s).withDensity f B

theorem MeasureTheory.VectorMeasure.variation_WithDensity_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} {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} : (μ.withDensity f B).variation ≤ (μ.transpose B).variation.withDensity fun (x : X) => ‖f x‖ₑ

theorem MeasureTheory.VectorMeasure.variation_withDensity' {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} [CompleteSpace G] (hf : μ.Integrable f) (hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊) : (μ.withDensity f B).variation = (μ.transpose B).variation.withDensity fun (x : X) => ‖f x‖ₑ

If ‖B x y‖ = ‖B · y‖ * ‖x‖ for all x, y, then the variation of a vector measure with density f wrt μ is the measure with density ‖f‖ₑ with respect to the variation of μ.

The condition on B is necessary: for a counterexample without it, let B be the scalar product in ℝ² and f x everywhere horizontal and μ s everywhere vertical. Then μ.withDensity f B = 0 so its variation is zero, while the integral of ‖f‖ₑ is not.

See also variation_withDensity under the very common condition ‖B x y‖ = ‖x‖ ‖y‖.

theorem MeasureTheory.VectorMeasure.variation_withDensity {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} [CompleteSpace G] (hf : μ.Integrable f) (hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖x‖₊ * ‖y‖₊) : (μ.withDensity f B).variation = (μ.transpose B).variation.withDensity fun (x : X) => ‖f x‖ₑ

If ‖B x y‖ = ‖x‖ * ‖y‖ for all x, y, then the variation of a vector measure with density f wrt μ is the measure with density ‖f‖ₑ with respect to the variation of μ.

The condition on B is necessary: for a counterexample without it, let B be the scalar product in ℝ² and f x everywhere horizontal and μ s everywhere vertical. Then μ.withDensity f B = 0 so its variation is zero, while the integral of ‖f‖ₑ is not.

theorem MeasureTheory.Measure.variation_withDensityᵥ {X : Type u_1} {E : Type u_2} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure X} {f : X → E} (hf : Integrable f μ) : (μ.withDensityᵥ f).variation = μ.withDensity fun (x : X) => ‖f x‖ₑ

The variation of a vecture measure with density f with respect to a positive measure μ is the measure with density ‖f‖ₑ with respect to μ.