# mathlibdocumentation

measure_theory.measure.with_density_vector_measure

# 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 #

• measure_theory.measure.with_densityᵥ: 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 measure_theory.measure.with_densityᵥ {α : Type u_1} {E : Type u_3} [normed_group E] [ E] [borel_space E] {m : measurable_space α} (μ : measure_theory.measure α) (f : α → E) :

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

Equations
theorem measure_theory.with_densityᵥ_apply {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f : α → E} (hf : μ) {s : set α} (hs : measurable_set s) :
(μ.with_densityᵥ f) s = (x : α) in s, f x μ
@[simp]
theorem measure_theory.with_densityᵥ_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] :
= 0
@[simp]
theorem measure_theory.with_densityᵥ_neg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f : α → E} :
theorem measure_theory.with_densityᵥ_neg' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f : α → E} :
μ.with_densityᵥ (λ (x : α), -f x) = -
@[simp]
theorem measure_theory.with_densityᵥ_add {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
μ.with_densityᵥ (f + g) = +
theorem measure_theory.with_densityᵥ_add' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
μ.with_densityᵥ (λ (x : α), f x + g x) = +
@[simp]
theorem measure_theory.with_densityᵥ_sub {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
μ.with_densityᵥ (f - g) = -
theorem measure_theory.with_densityᵥ_sub' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
μ.with_densityᵥ (λ (x : α), f x - g x) = -
@[simp]
theorem measure_theory.with_densityᵥ_smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {𝕜 : Type u_2} [ E] [ E] (f : α → E) (r : 𝕜) :
μ.with_densityᵥ (r f) = r
theorem measure_theory.with_densityᵥ_smul' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {𝕜 : Type u_2} [ E] [ E] (f : α → E) (r : 𝕜) :
μ.with_densityᵥ (λ (x : α), r f x) = r
theorem measure_theory.integrable.ae_eq_of_with_densityᵥ_eq {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) (hfg : = ) :
f =ᵐ[μ] g

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

theorem measure_theory.with_densityᵥ_eq.congr_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f g : α → E} (h : f =ᵐ[μ] g) :
=
theorem measure_theory.integrable.with_densityᵥ_eq_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f g : α → E} (hf : μ) (hg : μ) :
= f =ᵐ[μ] g
theorem measure_theory.with_densityᵥ_to_real {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hfm : μ) (hf : ∫⁻ (x : α), f x μ ) :
μ.with_densityᵥ (λ (x : α), (f x).to_real) =
theorem measure_theory.integrable.with_densityᵥ_trim_eq_integral {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α → } (hf : μ) {i : set α} (hi : measurable_set i) :
((μ.with_densityᵥ f).trim hm) i = (x : α) in i, f x μ
theorem measure_theory.integrable.with_densityᵥ_trim_absolutely_continuous {α : Type u_1} {E : Type u_3} [normed_group E] [ E] [borel_space E] {f : α → E} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (hfi : μ) :