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 functionfwith respect to a measureμon some set iffis integrable, and0otherwise.
def
MeasureTheory.Measure.withDensityᵥ
{α : Type u_1}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(f : α → E)
:
Given a measure μ and an integrable function f, μ.withDensityᵥ f is
the vector measure which maps the set s to ∫ₛ f ∂μ.
Instances For
theorem
MeasureTheory.withDensityᵥ_apply
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
(hf : MeasureTheory.Integrable f)
{s : Set α}
(hs : MeasurableSet s)
:
↑(MeasureTheory.Measure.withDensityᵥ μ f) s = ∫ (x : α) in s, f x ∂μ
@[simp]
theorem
MeasureTheory.withDensityᵥ_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
:
@[simp]
theorem
MeasureTheory.withDensityᵥ_neg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
:
theorem
MeasureTheory.withDensityᵥ_neg'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
:
(MeasureTheory.Measure.withDensityᵥ μ fun x => -f x) = -MeasureTheory.Measure.withDensityᵥ μ f
@[simp]
theorem
MeasureTheory.withDensityᵥ_add
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
theorem
MeasureTheory.withDensityᵥ_add'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
(MeasureTheory.Measure.withDensityᵥ μ fun x => f x + g x) = MeasureTheory.Measure.withDensityᵥ μ f + MeasureTheory.Measure.withDensityᵥ μ g
@[simp]
theorem
MeasureTheory.withDensityᵥ_sub
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
theorem
MeasureTheory.withDensityᵥ_sub'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
(MeasureTheory.Measure.withDensityᵥ μ fun x => f x - g x) = MeasureTheory.Measure.withDensityᵥ μ f - MeasureTheory.Measure.withDensityᵥ μ g
@[simp]
theorem
MeasureTheory.withDensityᵥ_smul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{𝕜 : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[SMulCommClass ℝ 𝕜 E]
(f : α → E)
(r : 𝕜)
:
MeasureTheory.Measure.withDensityᵥ μ (r • f) = r • MeasureTheory.Measure.withDensityᵥ μ f
theorem
MeasureTheory.withDensityᵥ_smul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{𝕜 : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[SMulCommClass ℝ 𝕜 E]
(f : α → E)
(r : 𝕜)
:
(MeasureTheory.Measure.withDensityᵥ μ fun x => r • f x) = r • MeasureTheory.Measure.withDensityᵥ μ f
theorem
MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous
{α : Type u_1}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(f : α → ℝ)
:
theorem
MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
(hfg : MeasureTheory.Measure.withDensityᵥ μ f = MeasureTheory.Measure.withDensityᵥ μ g)
:
Having the same density implies the underlying functions are equal almost everywhere.
theorem
MeasureTheory.WithDensityᵥEq.congr_ae
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
{g : α → E}
(h : f =ᶠ[MeasureTheory.Measure.ae μ] g)
:
theorem
MeasureTheory.Integrable.withDensityᵥ_eq_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
theorem
MeasureTheory.withDensityᵥ_toReal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hfm : AEMeasurable f)
(hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
:
theorem
MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hfi : MeasureTheory.Integrable f)
:
theorem
MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
{f : α → ℝ}
(hf : MeasureTheory.Integrable f)
{i : Set α}
(hi : MeasurableSet i)
:
↑(MeasureTheory.VectorMeasure.trim (MeasureTheory.Measure.withDensityᵥ μ f) hm) i = ∫ (x : α) in i, f x ∂μ
theorem
MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous
{α : Type u_1}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(hfi : MeasureTheory.Integrable f)
: