Documentation

Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure

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 #

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
    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) :
    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 : 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 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