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 #

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] [measurable_space E] [topological_space.second_countable_topology E] [normed_space E] [complete_space E] [borel_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ᵥ_smul' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_group E] [measurable_space E] [topological_space.second_countable_topology E] [normed_space E] [complete_space E] [borel_space E] {𝕜 : Type u_2} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [smul_comm_class 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] (f : α → E) (r : 𝕜) :
μ.with_densityᵥ (λ (x : α), r f x) = r μ.with_densityᵥ f

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

theorem measure_theory.with_densityᵥ_to_real {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (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 μ