Vector measure defined by an integral #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 functionfwith respect to a measureμon some set iffis integrable, and0otherwise.
noncomputable
def
measure_theory.measure.with_densityᵥ
{α : Type u_1}
{E : Type u_3}
[normed_add_comm_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
- μ.with_densityᵥ f = dite (measure_theory.integrable f μ) (λ (hf : measure_theory.integrable f μ), {measure_of' := λ (s : set α), ite (measurable_set s) (∫ (x : α) in s, f x ∂μ) 0, empty' := _, not_measurable' := _, m_Union' := _}) (λ (hf : ¬measure_theory.integrable f μ), 0)
theorem
measure_theory.with_densityᵥ_apply
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f : α → E}
(hf : measure_theory.integrable f μ)
{s : set α}
(hs : measurable_set s) :
@[simp]
theorem
measure_theory.with_densityᵥ_zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E] :
μ.with_densityᵥ 0 = 0
@[simp]
theorem
measure_theory.with_densityᵥ_neg
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f : α → E} :
μ.with_densityᵥ (-f) = -μ.with_densityᵥ f
theorem
measure_theory.with_densityᵥ_neg'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_3}
[normed_add_comm_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_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f g : α → E}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
μ.with_densityᵥ (f + g) = μ.with_densityᵥ f + μ.with_densityᵥ g
theorem
measure_theory.with_densityᵥ_add'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_3}
[normed_add_comm_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_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f g : α → E}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
μ.with_densityᵥ (f - g) = μ.with_densityᵥ f - μ.with_densityᵥ g
theorem
measure_theory.with_densityᵥ_sub'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_3}
[normed_add_comm_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_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{𝕜 : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[smul_comm_class ℝ 𝕜 E]
(f : α → E)
(r : 𝕜) :
μ.with_densityᵥ (r • f) = r • μ.with_densityᵥ f
theorem
measure_theory.with_densityᵥ_smul'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{𝕜 : Type u_2}
[nontrivially_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.measure.with_densityᵥ_absolutely_continuous
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
(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_add_comm_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) :
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_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f g : α → E}
(h : f =ᵐ[μ] g) :
μ.with_densityᵥ f = μ.with_densityᵥ g
theorem
measure_theory.integrable.with_densityᵥ_eq_iff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f g : α → E}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
μ.with_densityᵥ f = μ.with_densityᵥ g ↔ 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.with_densityᵥ_eq_with_density_pos_part_sub_with_density_neg_part
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hfi : measure_theory.integrable f μ) :
μ.with_densityᵥ f = (μ.with_density (λ (x : α), ennreal.of_real (f x))).to_signed_measure - (μ.with_density (λ (x : α), ennreal.of_real (-f x))).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) :
theorem
measure_theory.integrable.with_densityᵥ_trim_absolutely_continuous
{α : Type u_1}
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f : α → E}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(hfi : measure_theory.integrable f μ) :
((μ.with_densityᵥ f).trim hm).absolutely_continuous (μ.trim hm).to_ennreal_vector_measure