MeasureTheory.SignedMeasure.integrable_rnDeriv
theorem MeasureTheory.SignedMeasure.integrable_rnDeriv :
∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
MeasureTheory.Integrable (s.rnDeriv μ) μ
The theorem `MeasureTheory.SignedMeasure.integrable_rnDeriv` states that for any given `MeasurableSpace` α and a `SignedMeasure` s on α, and for any `Measure` μ on α, the Radon-Nikodym derivative of the `SignedMeasure` s with respect to the `Measure` μ, denoted as `MeasureTheory.SignedMeasure.rnDeriv s μ`, is integrable with respect to μ. In mathematical terms, it means that the function `MeasureTheory.SignedMeasure.rnDeriv s μ` is measurable and has a finite integral over the measure space α with respect to the measure μ.
More concisely: The Radon-Nikodym derivative of a signed measure with respect to a given measure is integrable with respect to the measure.
|
MeasureTheory.SignedMeasure.eq_rnDeriv
theorem MeasureTheory.SignedMeasure.eq_rnDeriv :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : MeasureTheory.SignedMeasure α}
(t : MeasureTheory.SignedMeasure α) (f : α → ℝ),
MeasureTheory.Integrable f μ →
MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure →
s = t + μ.withDensityᵥ f → μ.ae.EventuallyEq f (s.rnDeriv μ)
Given a measurable space `α`, a measure `μ` on `α`, signed measures `s` and `t` on `α`, and a real-valued function `f` on `α` that is integrable with respect to `μ`, if `t` is mutually singular with respect to `μ` (i.e., they give zero measure to the same sets), and `s` is the sum of `t` and the vector measure derived from `μ` with density `f`, then `f` equals the Radon-Nikodym derivative of `s` with respect to `μ` almost everywhere. The Radon-Nikodym derivative of `s` with respect to `μ` represents the change in `s` for each infinitesimal change in `μ`, which in this case is shown to be `f`.
More concisely: If `μ` is a measure on a measurable space `α`, `f` is an integrable real-valued function on `α`, `s` and `t` are signed measures on `α` with `μ`-mutually singular supports, and `s = t + ∫(f)dμ`, then `f` is the Radon-Nikodym derivative of `s` with respect to `μ` almost everywhere.
|
MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq
theorem MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : MeasureTheory.SignedMeasure α)
[inst : s.HaveLebesgueDecomposition μ], s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s
The theorem, named "MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq", is a statement of the Lebesgue Decomposition theorem for a signed measure and a measure. It states that for any given signed measure 's' and a σ-finite measure 'μ', there exist a signed measure 't' and a measurable, integrable function 'f', such that 't' is mutually singular with respect to 'μ', and 's' can be expressed as the sum of 't' and the product of 'μ' and the density function 'f'. This theorem further states that in this case, 't' is equivalent to the singular part of 's' with respect to 'μ', and 'f' is equivalent to the Radon-Nikodym derivative of 's' with respect to 'μ'.
More concisely: For any signed measure 's' and σ-finite measure 'μ', there exists a signed measure 't' mutually singular with 'μ' and a measurable, integrable function 'f' such that 's' = 't' + 'μ'∘'f'.
|
MeasureTheory.SignedMeasure.eq_singularPart
theorem MeasureTheory.SignedMeasure.eq_singularPart :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : MeasureTheory.SignedMeasure α}
(t : MeasureTheory.SignedMeasure α) (f : α → ℝ),
MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure →
s = t + μ.withDensityᵥ f → t = s.singularPart μ
This theorem states that, given a measure `μ`, signed measures `s` and `t`, and a function `f` such that `t` is mutually singular with respect to `μ` and `s` is equal to the sum of `t` and the vector measure associated with the density function `f` relative to `μ`, then `t` is the singular part of the Lebesgue decomposition between `s` and `μ`. In other words, if we have a signed measure `s` that can be decomposed into a part `t` that is mutually singular with `μ` and another part associated with a density function `f`, then `t` is exactly the singular part of the decomposition between `s` and `μ` according to Lebesgue's theorem on measures.
More concisely: Given a measure `μ`, signed measures `s` and `t`, and a function `f`, if `t` is mutually singular with `μ`, `s = t + µ(|f|)`, then `t` is the singular part of the Lebesgue decomposition of `s` with respect to `μ`.
|