# 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 function `f` with respect to a measure `μ` on some set if `f` is integrable, and `0` otherwise.

source
def MeasureTheory.Measure.withDensityᵥ {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} (μ : Measure α) (f : α → E) :
VectorMeasure α E

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem MeasureTheory.withDensityᵥ_apply {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} (hf : Integrable f μ) {s : Set α} (hs : MeasurableSet s) :
↑(μ.withDensityᵥ f) s = ∫ (x : α) in s, f x ∂μ
source
@[simp]
theorem MeasureTheory.withDensityᵥ_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] :
μ.withDensityᵥ 0 = 0
source
@[simp]
theorem MeasureTheory.withDensityᵥ_neg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} :
μ.withDensityᵥ (-f) = -μ.withDensityᵥ f
source
theorem MeasureTheory.withDensityᵥ_neg' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} :
(μ.withDensityᵥ fun (x : α) => -f x) = -μ.withDensityᵥ f
source
@[simp]
theorem MeasureTheory.withDensityᵥ_add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) :
μ.withDensityᵥ (f + g) = μ.withDensityᵥ f + μ.withDensityᵥ g
source
theorem MeasureTheory.withDensityᵥ_add' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) :
(μ.withDensityᵥ fun (x : α) => f x + g x) = μ.withDensityᵥ f + μ.withDensityᵥ g
source
@[simp]
theorem MeasureTheory.withDensityᵥ_sub {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) :
μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g
source
theorem MeasureTheory.withDensityᵥ_sub' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) :
(μ.withDensityᵥ fun (x : α) => f x - g x) = μ.withDensityᵥ f - μ.withDensityᵥ g
source
@[simp]
theorem MeasureTheory.withDensityᵥ_smul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] (f : α → E) (r : 𝕜) :
μ.withDensityᵥ (r • f) = r • μ.withDensityᵥ f
source
theorem MeasureTheory.withDensityᵥ_smul' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] (f : α → E) (r : 𝕜) :
(μ.withDensityᵥ fun (x : α) => r • f x) = r • μ.withDensityᵥ f
source
theorem MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} {g : α → E} (hf : AEMeasurable f μ) (hfg : Integrable (f • g) μ) :
μ.withDensityᵥ (f • g) = (μ.withDensity fun (x : α) => ↑(f x)).withDensityᵥ g
source
theorem MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → ENNReal} {g : α → E} (hf : AEMeasurable f μ) (hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤) (hfg : Integrable (fun (x : α) => (f x).toReal • g x) μ) :
(μ.withDensityᵥ fun (x : α) => (f x).toReal • g x) = (μ.withDensity f).withDensityᵥ g
source
theorem MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) (f : α → ℝ) :
(μ.withDensityᵥ f).AbsolutelyContinuous μ.toENNRealVectorMeasure
source
theorem MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) (hfg : μ.withDensityᵥ f = μ.withDensityᵥ g) :
f =ᶠ[ae μ] g

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

source
theorem MeasureTheory.WithDensityᵥEq.congr_ae {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : α → E} (h : f =ᶠ[ae μ] g) :
μ.withDensityᵥ f = μ.withDensityᵥ g
source
theorem MeasureTheory.Integrable.withDensityᵥ_eq_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) :
μ.withDensityᵥ f = μ.withDensityᵥ g ↔ f =ᶠ[ae μ] g
source
theorem MeasureTheory.withDensityᵥ_toReal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hfm : AEMeasurable f μ) (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) :
(μ.withDensityᵥ fun (x : α) => (f x).toReal) = (μ.withDensity f).toSignedMeasure
source
theorem MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hfi : Integrable f μ) :
μ.withDensityᵥ f = (μ.withDensity fun (x : α) => ENNReal.ofReal (f x)).toSignedMeasure - (μ.withDensity fun (x : α) => ENNReal.ofReal (-f x)).toSignedMeasure
source
theorem MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) {f : α → ℝ} (hf : Integrable f μ) {i : Set α} (hi : MeasurableSet i) :
↑((μ.withDensityᵥ f).trim hm) i = ∫ (x : α) in i, f x ∂μ
source
theorem MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (hfi : Integrable f μ) :
((μ.withDensityᵥ f).trim hm).AbsolutelyContinuous (μ.trim hm).toENNRealVectorMeasure