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.

def MeasureTheory.Measure.withDensityᵥ {α : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → E) : MeasureTheory.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.

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) : ↑(μ.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] : μ.withDensityᵥ 0 = 0

@[simp]

theorem MeasureTheory.withDensityᵥ_neg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} : μ.withDensityᵥ (-f) = -μ.withDensityᵥ f

theorem MeasureTheory.withDensityᵥ_neg' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} : (μ.withDensityᵥ fun (x : α) => -f x) = -μ.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 μ) : μ.withDensityᵥ (f + g) = μ.withDensityᵥ f + μ.withDensityᵥ 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 μ) : (μ.withDensityᵥ fun (x : α) => f x + g x) = μ.withDensityᵥ f + μ.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 μ) : μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ 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 μ) : (μ.withDensityᵥ fun (x : α) => f x - g x) = μ.withDensityᵥ f - μ.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 : 𝕜) : μ.withDensityᵥ (r • f) = r • μ.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 : 𝕜) : (μ.withDensityᵥ fun (x : α) => r • f x) = r • μ.withDensityᵥ f

theorem MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} {g : α → E} (hf : AEMeasurable f μ) (hfg : MeasureTheory.Integrable (f • g) μ) : μ.withDensityᵥ (f • g) = (μ.withDensity fun (x : α) => ↑(f x)).withDensityᵥ g

theorem MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → ENNReal} {g : α → E} (hf : AEMeasurable f μ) (hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤) (hfg : MeasureTheory.Integrable (fun (x : α) => (f x).toReal • g x) μ) : (μ.withDensityᵥ fun (x : α) => (f x).toReal • g x) = (μ.withDensity f).withDensityᵥ g

theorem MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ) : (μ.withDensityᵥ f).AbsolutelyContinuous μ.toENNRealVectorMeasure

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 : μ.withDensityᵥ f = μ.withDensityᵥ g) : μ.ae.EventuallyEq f 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 : μ.ae.EventuallyEq f g) : μ.withDensityᵥ f = μ.withDensityᵥ 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 μ) : μ.withDensityᵥ f = μ.withDensityᵥ g ↔ μ.ae.EventuallyEq f g

theorem MeasureTheory.withDensityᵥ_toReal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hfm : AEMeasurable f μ) (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : (μ.withDensityᵥ fun (x : α) => (f x).toReal) = (μ.withDensity f).toSignedMeasure

theorem MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hfi : MeasureTheory.Integrable f μ) : μ.withDensityᵥ f = (μ.withDensity fun (x : α) => ENNReal.ofReal (f x)).toSignedMeasure - (μ.withDensity fun (x : α) => ENNReal.ofReal (-f x)).toSignedMeasure

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) : ↑((μ.withDensityᵥ f).trim 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 μ) : ((μ.withDensityᵥ f).trim hm).AbsolutelyContinuous (μ.trim hm).toENNRealVectorMeasure