MeasureTheory.Measure.withDensity_rnDeriv_eq
theorem MeasureTheory.Measure.withDensity_rnDeriv_eq :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : μ.HaveLebesgueDecomposition ν],
μ.AbsolutelyContinuous ν → ν.withDensity (μ.rnDeriv ν) = μ
This theorem states that for any two measures `μ` and `ν` on a measurable space `α`, if `μ` has a Lebesgue decomposition with respect to `ν`, and `μ` is absolutely continuous with respect to `ν`, then `ν` with density equal to the Radon-Nikodym derivative of `μ` with respect to `ν` is equal to `μ`. In simpler terms, given two measures, if one is absolutely continuous with respect to the other and a certain decomposition condition is met, then we can represent one measure as the other measure "scaled" by a specific function, which is the Radon-Nikodym derivative.
More concisely: If measure `μ` has a Lebesgue decomposition with respect to `ν` and is absolutely continuous with respect to `ν`, then `μ = ν ∣𝒫(dμ∕dν)∣`.
|
MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular'
theorem MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular' :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite μ]
[inst : MeasureTheory.SigmaFinite ν] [inst : MeasureTheory.SigmaFinite ν'],
μ.MutuallySingular ν' → ν.MutuallySingular ν' → ν.ae.EventuallyEq (μ.rnDeriv (ν + ν')) (μ.rnDeriv ν)
This theorem, named `MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular'`, states that for any measurable space `α`, measures `μ`, `ν`, and `ν'` that are sigma finite, if `μ` and `ν` are both mutually singular with `ν'`, then the Radon-Nikodym derivative of `μ` with respect to the sum of `ν` and `ν'` is almost everywhere equal to the Radon-Nikodym derivative of `μ` with respect to `ν`. In essence, if two measures are each mutually singular with a third measure, adding the third measure doesn't affect the Radon-Nikodym derivative of the first measure with respect to the second.
More concisely: If `μ`, `ν`, and `ν'` are sigma-finite measures on a measurable space `α` such that `μ` and `ν` are mutually singular with `ν'`, then `dμ/d(ν + ν')` almost everywhere equals `dμ/dν`.
|
MeasureTheory.Measure.rnDeriv_withDensity_right_of_absolutelyContinuous
theorem MeasureTheory.Measure.rnDeriv_withDensity_right_of_absolutelyContinuous :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
{ν : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite μ] [inst : MeasureTheory.SigmaFinite ν],
μ.AbsolutelyContinuous ν →
AEMeasurable f ν →
(∀ᵐ (x : α) ∂ν, f x ≠ 0) →
(∀ᵐ (x : α) ∂ν, f x ≠ ⊤) →
ν.ae.EventuallyEq (μ.rnDeriv (ν.withDensity f)) fun x => (f x)⁻¹ * μ.rnDeriv ν x
This theorem, named "MeasureTheory.Measure.rnDeriv_withDensity_right_of_absolutelyContinuous", states that for any types `α` of a set, `m` as the measurable space, `μ` and `ν` as two sigma-finite measures on the measurable space, and `f` as a function mapping elements of the set `α` to the extended nonnegative real numbers (ENNReal), if `μ` is absolutely continuous with respect to `ν` (represented by `μ.AbsolutelyContinuous ν`), `f` is almost everywhere measurable with respect to `ν` (represented by `AEMeasurable f ν`), `f` is nonzero almost everywhere (represented by `∀ᵐ (x : α) ∂ν, f x ≠ 0`), and `f` is not infinity almost everywhere (represented by `∀ᵐ (x : α) ∂ν, f x ≠ ⊤`), then, almost everywhere, the Radon-Nikodym derivative of `μ` with respect to the measure induced by `ν` with a density function `f`, is equivalent to the product of the reciprocal of `f` and the Radon-Nikodym derivative of `μ` with respect to `ν` (represented by `ν.ae.EventuallyEq (μ.rnDeriv (ν.withDensity f)) fun x => (f x)⁻¹ * μ.rnDeriv ν x`).
More concisely: Given sigma-finite measures `μ` and `ν` on a measurable space, if `μ` is absolutely continuous with respect to `ν`, `f` is a nonzero, almost everywhere defined and measurable function from the domain of `μ` to the extended nonnegative real numbers, then almost everywhere, `μ`'s Radon-Nikodym derivative with respect to `ν` is equivalent to the product of the reciprocal of `f` and `μ`'s Radon-Nikodym derivative with respect to `ν`.
|
MeasureTheory.Measure.rnDeriv_pos
theorem MeasureTheory.Measure.rnDeriv_pos :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : μ.HaveLebesgueDecomposition ν],
μ.AbsolutelyContinuous ν → ∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x
This theorem states that for any type `α` and measurable space `m`, given two measures `μ` and `ν` on this space, if `μ` has a Lebesgue decomposition with respect to `ν`, and if `μ` is absolutely continuous with respect to `ν`, then almost everywhere with respect to the measure `μ`, the Radon-Nikodym derivative of `μ` with respect to `ν` is greater than zero.
In other words, this theorem is about the positive nature of the Radon-Nikodym derivative under the condition of absolute continuity. In mathematical terms, if `μ` is absolutely continuous with respect to `ν` (i.e., whenever `ν(A) = 0` it implies `μ(A) = 0` for any subset `A` of the measurable space), then the Radon-Nikodym derivative `μ.rnDeriv ν x` is almost everywhere positive with respect to the measure `μ`.
More concisely: If `μ` is an absolutely continuous measure with respect to `ν` in a measurable space, then the Radon-Nikodym derivative `μ.rnDeriv ν` is almost everywhere positive with respect to `μ`.
|
MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq
theorem MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq :
∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
[inst : MeasureTheory.SigmaFinite μ],
MeasureTheory.VectorMeasure.AbsolutelyContinuous s μ.toENNRealVectorMeasure ↔ μ.withDensityᵥ (s.rnDeriv μ) = s
The Radon-Nikodym theorem for signed measures states that, for any measurable space `α`, a signed measure `s` on `α`, and a sigma-finite measure `μ` on `α`, `s` is absolutely continuous with respect to `μ`'s associated ennreal vector measure if and only if the vector measure associated with the density of `s` with respect to `μ` equals `s`.
In other words, a signed measure `s` is absolutely continuous with respect to a sigma-finite measure `μ` if any set whose measure under `μ` is zero also has measure zero under `s`. This property is equivalent to `s` being equal to the vector measure obtained by weighting `μ` according to the Radon-Nikodym derivative of `s` with respect to `μ`.
More concisely: A signed measure is absolutely continuous with respect to a sigma-finite measure if and only if it is equal to the vector measure obtained by integrating the measure with respect to its Radon-Nikodym derivative.
|
MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_left
theorem MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_left :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ENNReal} (μ ν : MeasureTheory.Measure α)
[inst : MeasureTheory.SigmaFinite μ] [inst : MeasureTheory.SigmaFinite ν],
AEMeasurable f μ →
(∀ᵐ (x : α) ∂μ, f x ≠ ⊤) →
ν.ae.EventuallyEq (((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν) ((μ.withDensity f).rnDeriv ν)
This theorem, `MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_left`, states that for any measurable space `α`, any function `f` from `α` to the extended nonnegative real numbers, and any two sigma-finite measures `μ` and `ν` on `α`, if `f` is almost everywhere measurable with respect to `μ` and `f` is not equal to `∞` almost everywhere with respect to `μ`, then almost everywhere with respect to `ν`, the Radon-Nikodym derivative of `ν` with respect to the measure obtained by applying `f` as a density to the measure obtained by applying the Radon-Nikodym derivative of `ν` with respect to `μ` as a density to `ν`, is equal to the Radon-Nikodym derivative of `ν` with respect to the measure obtained by applying `f` as a density to `μ`. The theorem is used as an auxiliary lemma for proving another theorem `rnDeriv_withDensity_left`.
More concisely: Given measurable spaces `α`, measurable functions `f : α → [0, ∞]`, and sigma-finite measures `μ` and `ν` on `α` with `f` almost everywhere defined and finite with respect to `μ`, the Radon-Nikodym derivatives of `ν` with respect to the measures obtained using `μ` and `ν` as bases and `f` as densities are equal almost everywhere.
|
MeasureTheory.Measure.rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular
theorem MeasureTheory.Measure.rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite μ]
[inst : MeasureTheory.SigmaFinite ν] [inst : MeasureTheory.SigmaFinite ν'],
μ.AbsolutelyContinuous ν → ν.MutuallySingular ν' → ν.ae.EventuallyEq (μ.rnDeriv (ν + ν')) (μ.rnDeriv ν)
This theorem, `MeasureTheory.Measure.rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular`, states that for any type `α`, measurable space `m`, and measures `μ`, `ν`, and `ν'` (with `μ`, `ν`, and `ν'` being sigma-finite), if `μ` is absolutely continuous with respect to `ν`, and `ν` is mutually singular with `ν'`, then almost everywhere, the Radon-Nikodym derivative of `μ` with respect to `ν + ν'` is equal to the Radon-Nikodym derivative of `μ` with respect to `ν`. The Radon-Nikodym derivative is a concept from measure theory that gives a way to "divide" one measure by another in a sense.
More concisely: If measures `μ` and `ν` are sigma-finite, `μ` is absolutely continuous with respect to `ν`, and `ν` is mutually singular with `ν'`, then `μ`'s Radon-Nikodym derivative with respect to `ν + ν'` equals its Radon-Nikodym derivative with respect to `ν` almost everywhere.
|
MeasureTheory.Measure.rnDeriv_withDensity_left
theorem MeasureTheory.Measure.rnDeriv_withDensity_left :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ENNReal} {μ ν : MeasureTheory.Measure α}
[inst : MeasureTheory.SigmaFinite μ] [inst : MeasureTheory.SigmaFinite ν],
AEMeasurable f μ →
AEMeasurable f ν →
(∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → ν.ae.EventuallyEq ((μ.withDensity f).rnDeriv ν) fun x => f x * μ.rnDeriv ν x
This theorem, `MeasureTheory.Measure.rnDeriv_withDensity_left`, states that for any given measurable space `α`, a function `f : α → ENNReal` (mapping elements of `α` to extended nonnegative real numbers), and two sigma-finite measures `μ` and `ν` on `α`, if `f` is almost everywhere measurable with respect to both `μ` and `ν`, and `f` is almost everywhere finite with respect to `μ`, then the Radon-Nikodym derivative of the measure obtained by scaling `μ` by `f` with respect to `ν`, is almost everywhere equal (with respect to `ν`) to the function that maps `x` in `α` to the product of `f(x)` and the Radon-Nikodym derivative of `μ` with respect to `ν` at `x`.
In simpler terms, it relates the Radon-Nikodym derivative of a weighted measure to the weight function and the Radon-Nikodym derivative of the original measure, under certain conditions on the weight function and the measures.
More concisely: Given measurable spaces `α`, a sigma-finite measure `μ`, a sigma-finite measure `ν`, a measurable function `f : α → ENNReal` that is almost everywhere finite and measurable with respect to both `μ` and `ν`, the Radon-Nikodym derivative `d(μ / f) / dν` almost everywhere equals the product of `f` and the Radon-Nikodym derivative `dμ / dν`.
|
MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_right
theorem MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_right :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ENNReal} (μ ν : MeasureTheory.Measure α)
[inst : MeasureTheory.SigmaFinite μ] [inst : MeasureTheory.SigmaFinite ν],
AEMeasurable f ν →
(∀ᵐ (x : α) ∂ν, f x ≠ 0) →
(∀ᵐ (x : α) ∂ν, f x ≠ ⊤) →
ν.ae.EventuallyEq ((ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f)) (μ.rnDeriv (ν.withDensity f))
The theorem `MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_right` states that for any type `α`, any measurable space `m` on `α`, any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), and any two sigma-finite measures `μ` and `ν` on `α`, if `f` is almost everywhere measurable with respect to measure `ν`, `f` is almost everywhere nonzero, and `f` is almost everywhere finite, then the Radon-Nikodym derivative of the measure `(ν.withDensity (μ.rnDeriv ν))` with respect to the measure `(ν.withDensity f)` is equal to the Radon-Nikodym derivative of `μ` with respect to the measure `(ν.withDensity f)` almost everywhere with respect to measure `ν`. The Radon-Nikodym derivative `μ.rnDeriv ν` is the derivative of measure `μ` with respect to measure `ν` and `ν.withDensity f` is the measure `ν` reweighted by the function `f`.
More concisely: For measurable spaces `(α, m)`, measurable functions `f : α → ENNReal`, and sigma-finite measures `μ` and `ν` on `α`, if `f` is almost everywhere measurable, almost everywhere nonzero, and almost everywhere finite with respect to `ν`, then `(μ.rnDeriv ν) = (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f)` almost everywhere with respect to `ν`.
|
MeasureTheory.Measure.inv_rnDeriv_aux
theorem MeasureTheory.Measure.inv_rnDeriv_aux :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite μ]
[inst : MeasureTheory.SigmaFinite ν],
μ.AbsolutelyContinuous ν → ν.AbsolutelyContinuous μ → μ.ae.EventuallyEq (μ.rnDeriv ν)⁻¹ (ν.rnDeriv μ)
This theorem, `MeasureTheory.Measure.inv_rnDeriv_aux`, states that for any type `α`, measurable space `m`, and measures `μ` and `ν` where `μ` and `ν` are both sigma-finite, if measure `μ` is absolutely continuous with respect to measure `ν` and vice versa, then almost everywhere (`μ.ae.EventuallyEq`), the Radon-Nikodym derivative of `μ` with respect to `ν` inversely equals the Radon-Nikodym derivative of `ν` with respect to `μ`. In other words, the reciprocal of the Radon-Nikodym derivative of `μ` with respect to `ν` is almost everywhere equal to the Radon-Nikodym derivative of `ν` with respect to `μ`.
More concisely: If measures `μ` and `ν` on measurable space `(α, m)` are sigma-finite, absolutely continuous with respect to each other, then their Radon-Nikodym derivatives are almost everywhere equal and their reciprocals are almost everywhere equal.
|
MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq
theorem MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : μ.HaveLebesgueDecomposition ν],
μ.AbsolutelyContinuous ν ↔ ν.withDensity (μ.rnDeriv ν) = μ
This theorem, known as the Radon-Nikodym Theorem, asserts that for any two measures `μ` and `ν` in a measurable space `α`, if `μ` has a Lebesgue decomposition with respect to `ν`, then `μ` is absolutely continuous with respect to `ν` if and only if the measure `ν` with density function defined by the Radon-Nikodym derivative of `μ` with respect to `ν` is equal to `μ`. This theorem provides a crucial relationship between the concept of absolute continuity and the Radon-Nikodym derivative in measure theory.
More concisely: The Radon-Nikodym Theorem states that for measures `μ` and `ν` in a measurable space, `μ` is absolutely continuous with respect to `ν` if and only if `μ = ν ∘ d(μ/ν)`, where `d(μ/ν)` is the Radon-Nikodym derivative of `μ` with respect to `ν`.
|
MeasureTheory.integrable_rnDeriv_smul_iff
theorem MeasureTheory.integrable_rnDeriv_smul_iff :
∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {E : Type u_4}
[inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : μ.HaveLebesgueDecomposition ν],
μ.AbsolutelyContinuous ν →
∀ [inst_3 : MeasureTheory.SigmaFinite μ] {f : α → E},
MeasureTheory.Integrable (fun x => (μ.rnDeriv ν x).toReal • f x) ν ↔ MeasureTheory.Integrable f μ
The theorem `MeasureTheory.integrable_rnDeriv_smul_iff` states that for any measure space `α`, a measure `μ`, another measure `ν`, a normed commutative additive group `E` which is also a normed space over the real numbers, and a function `f` from `α` to `E`, if `μ` is absolutely continuous with respect to `ν` and `μ` has a Lebesgue decomposition with respect to `ν`, then the function `f` scaled by the Radon-Nikodym derivative of `μ` with respect to `ν` is integrable with respect to `ν` if and only if `f` is integrable with respect to `μ`. Here, absolute continuity means that if a set has `ν`-measure zero, then it also has `μ`-measure zero. And integrability means that the function is both almost-everywhere strongly measurable and has a finite integral.
More concisely: For a measure space with absolutely continuous and Lebesgue decomposable measures μ and ν, and a function f from the measure space to a normed real vector space, the derivative of μ with respect to ν and the function f are interchangeable in integrability, i.e., f is integrable with respect to μ if and only if the scaled function f * (dμ/dν) is integrable with respect to ν.
|