mathlib documentation

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 #

noncomputable def measure_theory.measure.with_densityᵥ {α : Type u_1} {E : Type u_3} [normed_group E] [normed_space E] [complete_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] [normed_space E] [complete_space E] {f : α → E} (hf : measure_theory.integrable f μ) {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] [normed_space E] [complete_space E] :
@[simp]
theorem measure_theory.with_densityᵥ_neg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [normed_space E] [complete_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] [normed_space E] [complete_space E] {f : α → E} :
μ.with_densityᵥ (λ (x : α), -f x) = -μ.with_densityᵥ f
@[simp]
theorem measure_theory.with_densityᵥ_add {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [normed_space E] [complete_space E] {f g : α → E} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
theorem measure_theory.with_densityᵥ_add' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [normed_space E] [complete_space E] {f g : α → E} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
μ.with_densityᵥ (λ (x : α), f x + g x) = μ.with_densityᵥ f + μ.with_densityᵥ g
@[simp]
theorem measure_theory.with_densityᵥ_sub {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [normed_space E] [complete_space E] {f g : α → E} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
theorem measure_theory.with_densityᵥ_sub' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [normed_space E] [complete_space E] {f g : α → E} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
μ.with_densityᵥ (λ (x : α), f x - g x) = μ.with_densityᵥ f - μ.with_densityᵥ g
@[simp]
theorem measure_theory.with_densityᵥ_smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [normed_space E] [complete_space E] {𝕜 : Type u_2} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [smul_comm_class 𝕜 E] (f : α → E) (r : 𝕜) :
theorem measure_theory.with_densityᵥ_smul' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [normed_space E] [complete_space E] {𝕜 : Type u_2} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [smul_comm_class 𝕜 E] (f : α → E) (r : 𝕜) :
μ.with_densityᵥ (λ (x : α), r f x) = r μ.with_densityᵥ f
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] [normed_space E] [complete_space E] {f g : α → E} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) (hfg : μ.with_densityᵥ f = μ.with_densityᵥ g) :
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] [normed_space E] [complete_space E] {f g : α → E} (h : f =ᵐ[μ] g) :
theorem measure_theory.with_densityᵥ_to_real {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hfm : ae_measurable f μ) (hf : ∫⁻ (x : α), f x μ ) :
μ.with_densityᵥ (λ (x : α), (f x).to_real) = (μ.with_density f).to_signed_measure
theorem measure_theory.integrable.with_densityᵥ_trim_eq_integral {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α → } (hf : measure_theory.integrable f μ) {i : set α} (hi : measurable_set i) :
((μ.with_densityᵥ f).trim hm) i = (x : α) in i, f x μ