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) : ↑(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] : MeasureTheory.Measure.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} : MeasureTheory.Measure.withDensityᵥ μ (-f) = -MeasureTheory.Measure.withDensityᵥ μ f

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 μ) : MeasureTheory.Measure.withDensityᵥ μ (f + g) = MeasureTheory.Measure.withDensityᵥ μ f + MeasureTheory.Measure.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 μ) : (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 μ) : MeasureTheory.Measure.withDensityᵥ μ (f - g) = MeasureTheory.Measure.withDensityᵥ μ f - MeasureTheory.Measure.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 μ) : (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.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) μ) : MeasureTheory.Measure.withDensityᵥ μ (f • g) = MeasureTheory.Measure.withDensityᵥ (MeasureTheory.Measure.withDensity μ fun (x : α) => ↑(f x)) 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) μ) : (MeasureTheory.Measure.withDensityᵥ μ fun (x : α) => (f x).toReal • g x) = MeasureTheory.Measure.withDensityᵥ (MeasureTheory.Measure.withDensity μ f) g

theorem MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ) : MeasureTheory.VectorMeasure.AbsolutelyContinuous (MeasureTheory.Measure.withDensityᵥ μ f) (MeasureTheory.Measure.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 : MeasureTheory.Measure.withDensityᵥ μ f = MeasureTheory.Measure.withDensityᵥ μ g) : f =ᶠ[MeasureTheory.Measure.ae μ] 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) : MeasureTheory.Measure.withDensityᵥ μ f = MeasureTheory.Measure.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 μ) : MeasureTheory.Measure.withDensityᵥ μ f = MeasureTheory.Measure.withDensityᵥ μ g ↔ f =ᶠ[MeasureTheory.Measure.ae μ] g

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

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

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