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_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
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)
:
@[simp]
theorem
MeasureTheory.withDensityᵥ_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
:
@[simp]
theorem
MeasureTheory.withDensityᵥ_neg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
:
theorem
MeasureTheory.withDensityᵥ_neg'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → E}
:
@[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 μ)
:
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 μ)
:
@[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 μ)
:
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 μ)
:
@[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 : 𝕜)
:
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 : 𝕜)
:
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) μ)
:
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) μ)
:
theorem
MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous
{α : Type u_1}
{m : MeasurableSpace α}
(μ : Measure α)
(f : α → ℝ)
:
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)
:
Having the same density implies the underlying functions are equal almost everywhere.
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)
:
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 μ)
:
theorem
MeasureTheory.withDensityᵥ_toReal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : 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 α}
{μ : Measure α}
{f : α → ℝ}
(hfi : 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 m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
{f : α → ℝ}
(hf : Integrable f μ)
{i : Set α}
(hi : MeasurableSet i)
:
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