# Vector measure defined by an integral #

Given a measure μ and an integrable function f : α → E, we can define a vector measure v such that for all measurable set s, v i = ∫ x in s, f x ∂μ. This definition is useful for the Radon-Nikodym theorem for signed measures.

## Main definitions #

• MeasureTheory.Measure.withDensityᵥ: the vector measure formed by integrating a function f with respect to a measure μ on some set if f is integrable, and 0 otherwise.
def MeasureTheory.Measure.withDensityᵥ {α : Type u_1} {E : Type u_3} [] {m : } (μ : ) (f : αE) :

Given a measure μ and an integrable function f, μ.withDensityᵥ f is the vector measure which maps the set s to ∫ₛ f ∂μ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasureTheory.withDensityᵥ_apply {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {f : αE} (hf : ) {s : Set α} (hs : ) :
(μ.withDensityᵥ f) s = ∫ (x : α) in s, f xμ
@[simp]
theorem MeasureTheory.withDensityᵥ_zero {α : Type u_1} {m : } {μ : } {E : Type u_3} [] :
μ.withDensityᵥ 0 = 0
@[simp]
theorem MeasureTheory.withDensityᵥ_neg {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {f : αE} :
μ.withDensityᵥ (-f) = -μ.withDensityᵥ f
theorem MeasureTheory.withDensityᵥ_neg' {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {f : αE} :
(μ.withDensityᵥ fun (x : α) => -f x) = -μ.withDensityᵥ f
@[simp]
theorem MeasureTheory.withDensityᵥ_add {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {f : αE} {g : αE} (hf : ) (hg : ) :
μ.withDensityᵥ (f + g) = μ.withDensityᵥ f + μ.withDensityᵥ g
theorem MeasureTheory.withDensityᵥ_add' {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {f : αE} {g : αE} (hf : ) (hg : ) :
(μ.withDensityᵥ fun (x : α) => f x + g x) = μ.withDensityᵥ f + μ.withDensityᵥ g
@[simp]
theorem MeasureTheory.withDensityᵥ_sub {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {f : αE} {g : αE} (hf : ) (hg : ) :
μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g
theorem MeasureTheory.withDensityᵥ_sub' {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {f : αE} {g : αE} (hf : ) (hg : ) :
(μ.withDensityᵥ fun (x : α) => f x - g x) = μ.withDensityᵥ f - μ.withDensityᵥ g
@[simp]
theorem MeasureTheory.withDensityᵥ_smul {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {𝕜 : Type u_4} [] [] (f : αE) (r : 𝕜) :
μ.withDensityᵥ (r f) = r μ.withDensityᵥ f
theorem MeasureTheory.withDensityᵥ_smul' {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {𝕜 : Type u_4} [] [] (f : αE) (r : 𝕜) :
(μ.withDensityᵥ fun (x : α) => r f x) = r μ.withDensityᵥ f
theorem MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {f : αNNReal} {g : αE} (hf : ) (hfg : MeasureTheory.Integrable (f g) μ) :
μ.withDensityᵥ (f g) = (μ.withDensity fun (x : α) => (f x)).withDensityᵥ g
theorem MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity' {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {f : αENNReal} {g : αE} (hf : ) (hflt : ∀ᵐ (x : α) ∂μ, f x < ) (hfg : MeasureTheory.Integrable (fun (x : α) => (f x).toReal g x) μ) :
(μ.withDensityᵥ fun (x : α) => (f x).toReal g x) = (μ.withDensity f).withDensityᵥ g
theorem MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous {α : Type u_1} {m : } (μ : ) (f : α) :
(μ.withDensityᵥ f).AbsolutelyContinuous μ.toENNRealVectorMeasure
theorem MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq {α : Type u_1} {m : } {μ : } {E : Type u_3} [] [] {f : αE} {g : αE} (hf : ) (hg : ) (hfg : μ.withDensityᵥ f = μ.withDensityᵥ g) :
f =ᵐ[μ] g

Having the same density implies the underlying functions are equal almost everywhere.

theorem MeasureTheory.WithDensityᵥEq.congr_ae {α : Type u_1} {m : } {μ : } {E : Type u_3} [] {f : αE} {g : αE} (h : f =ᵐ[μ] g) :
μ.withDensityᵥ f = μ.withDensityᵥ g
theorem MeasureTheory.Integrable.withDensityᵥ_eq_iff {α : Type u_1} {m : } {μ : } {E : Type u_3} [] [] {f : αE} {g : αE} (hf : ) (hg : ) :
μ.withDensityᵥ f = μ.withDensityᵥ g f =ᵐ[μ] g
theorem MeasureTheory.withDensityᵥ_toReal {α : Type u_1} {m : } {μ : } {f : αENNReal} (hfm : ) (hf : ∫⁻ (x : α), f xμ ) :
(μ.withDensityᵥ fun (x : α) => (f x).toReal) = (μ.withDensity f).toSignedMeasure
theorem MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part {α : Type u_1} {m : } {μ : } {f : α} (hfi : ) :
μ.withDensityᵥ f = (μ.withDensity fun (x : α) => ENNReal.ofReal (f x)).toSignedMeasure - (μ.withDensity fun (x : α) => ENNReal.ofReal (-f x)).toSignedMeasure
theorem MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral {α : Type u_1} {m : } {m0 : } {μ : } (hm : m m0) {f : α} (hf : ) {i : Set α} (hi : ) :
((μ.withDensityᵥ f).trim hm) i = ∫ (x : α) in i, f xμ
theorem MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous {α : Type u_1} {E : Type u_3} [] {f : αE} {m : } {m0 : } {μ : } (hm : m m0) (hfi : ) :
((μ.withDensityᵥ f).trim hm).AbsolutelyContinuous (μ.trim hm).toENNRealVectorMeasure