MeasureTheory.Measure.rnDeriv_smul_left
theorem MeasureTheory.Measure.rnDeriv_smul_left :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν]
[inst : ν.HaveLebesgueDecomposition μ] (r : NNReal), μ.ae.EventuallyEq ((r • ν).rnDeriv μ) (r • ν.rnDeriv μ)
This theorem is about the Radon-Nikodym derivative of the scalar multiple of a measure. It states that for any measurable space `α`, given measures `ν` and `μ` on `α`, with `ν` being finite and having a Lebesgue decomposition with respect to `μ`, and a nonnegative real number `r`, the Radon-Nikodym derivative of `r • ν` with respect to `μ` is almost everywhere equal to `r •` the Radon-Nikodym derivative of `ν` with respect to `μ`.
In mathematical terms, if we denote the Radon-Nikodym derivative by the symbol `d/dμ`, then the theorem says that for almost every point in the space, `(d/dμ)(r • ν) = r • (d/dμ)ν`.
More concisely: For any measurable spaces `α`, finite measures `ν` and `μ` on `α` with `ν` having a Lebesgue decomposition with respect to `μ`, and a nonnegative real number `r`, the Radon-Nikodym derivatives `dν/dμ` and `d(r•ν)/dμ` almost everywhere agree and are equal to `r` times each other.
|
MeasureTheory.Measure.exists_positive_of_not_mutuallySingular
theorem MeasureTheory.Measure.exists_positive_of_not_mutuallySingular :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ]
[inst_1 : MeasureTheory.IsFiniteMeasure ν],
¬μ.MutuallySingular ν →
∃ ε,
0 < ε ∧
∃ E,
MeasurableSet E ∧
0 < ↑↑ν E ∧
MeasureTheory.VectorMeasure.restrict 0 E ≤
MeasureTheory.VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
In the context of measure theory, this theorem states that if two finite measures `μ` and `ν` are not mutually singular, there exists a positive real number `ε` and a measurable set `E` such that the `ν` measure of `E` is positive, and the `0`-restricted vector measure of `E` is less than or equal to the restricted vector measure of `E` with respect to the difference between the signed measures of `μ` and `ε` times `ν`. This theorem is particularly useful for the Lebesgue decomposition theorem. In simpler terms, if two measurement mechanisms aren't completely separate or independent, we can find a positive factor and a measurable subset where one measure outweighs a scaled version of the other.
More concisely: If two finite measures `μ` and `ν` are not mutually singular, there exists an `ε > 0` and a measurable set `E` such that `ν(E) > 0` and the total variation of `μ - εν` is less than or equal to the total variation of `μ` on `E`.
|
MeasureTheory.Measure.rnDeriv_def
theorem MeasureTheory.Measure.rnDeriv_def :
∀ {α : Type u_3} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
μ.rnDeriv ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).2 else 0
The theorem `MeasureTheory.Measure.rnDeriv_def` states that for any given measurable space `α` and two measures `μ` and `ν` on that space, the Radon-Nikodym derivative of `μ` with respect to `ν`, denoted as `μ.rnDeriv ν`, is defined as follows: If the measures `μ` and `ν` satisfy the Lebesgue Decomposition theorem (indicated by the existence proof `h : MeasureTheory.Measure.HaveLebesgueDecomposition μ ν`), then the Radon-Nikodym derivative is given by the second component of the pair returned by the function `Classical.choose`. This function selects an arbitrary element from a non-empty set that satisfies a certain property. If the measures `μ` and `ν` do not satisfy the Lebesgue Decomposition theorem, then the Radon-Nikodym derivative is defined as `0`.
More concisely: If measures `μ` and `ν` on measurable space `α` satisfy the Lebesgue Decomposition theorem, then `μ.rnDeriv ν` is the second component of the pair returned by `Classical.choose` on the set of Radon-Nikodym derivatives. Otherwise, `μ.rnDeriv ν` is `0`.
|
MeasureTheory.Measure.rnDeriv_smul_left'
theorem MeasureTheory.Measure.rnDeriv_smul_left' :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite ν]
[inst : MeasureTheory.SigmaFinite μ] (r : NNReal), μ.ae.EventuallyEq ((r • ν).rnDeriv μ) (r • ν.rnDeriv μ)
The theorem `MeasureTheory.Measure.rnDeriv_smul_left'` states that for any nonnegative real number `r` (represented as `NNReal`), and any two sigma-finite measures `ν` and `μ` on a measurable space `α`, the Radon-Nikodym derivative of the scalar multiplication of `ν` by `r` with respect to `μ` is almost everywhere equal to the scalar multiplication of the Radon-Nikodym derivative of `ν` with respect to `μ` by `r`. This theorem is a version of `rnDeriv_smul_left` that does not require `μ` to be finite, but requires both `ν` and `μ` to be sigma-finite measures.
In terms of mathematical notation, it states that for almost all `x` in the space `α`, `(r • ν).rnDeriv μ x = r • ν.rnDeriv μ x`.
More concisely: For sigma-finite measures ν and μ on a measurable space α, the Radon-Nikodym derivatives of ν with respect to μ almost everywhere satisfy (r · ν).rnDeriv μ = r · ν.rnDeriv μ for all nonnegative real numbers r.
|
MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top
theorem MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν]
[inst : ν.HaveLebesgueDecomposition μ] {r : ENNReal},
r ≠ 0 → r ≠ ⊤ → μ.ae.EventuallyEq (ν.rnDeriv (r • μ)) (r⁻¹ • ν.rnDeriv μ)
This theorem, known as the Radon-Nikodym derivative with respect to the scalar multiple of a measure, is applicable to a measurable space, denoted by `α`. The theorem specifically applies to two measures `ν` and `μ` on this space. The measures must fulfill the conditions that `ν` is a finite measure and it has a Lebesgue decomposition with respect to `μ`. A scalar `r` is involved, which belongs to the set of extended nonnegative real numbers, `ENNReal`, but is not equal to 0 or infinity. Given these conditions, the theorem states that the Radon-Nikodym derivative of `ν` with respect to the scalar multiple `r` of `μ`, is almost everywhere equal to the scalar multiple `r⁻¹` of the Radon-Nikodym derivative of `ν` with respect to `μ`. This theorem is particularly relevant when `ν` and `μ` are not sigma-finite.
More concisely: Given two finite measures `ν` and `μ` on a measurable space `α` with `ν` having a Lebesgue decomposition with respect to `μ`, the Radon-Nikodym derivatives of `ν` with respect to `μ` and `rμ` are almost everywhere equal, where `r` is a nonzero extended real number.
|
MeasureTheory.Measure.rnDeriv_add'
theorem MeasureTheory.Measure.rnDeriv_add' :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν₁ ν₂ μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite ν₁]
[inst : MeasureTheory.SigmaFinite ν₂] [inst : MeasureTheory.SigmaFinite μ],
μ.ae.EventuallyEq ((ν₁ + ν₂).rnDeriv μ) (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
This theorem states that for any three sigma-finite measures `ν₁`, `ν₂`, and `μ` on a measurable space `α`, the Radon-Nikodym derivative of the sum of `ν₁` and `ν₂` with respect to `μ` is almost everywhere equal to the sum of the Radon-Nikodym derivatives of `ν₁` and `ν₂` with respect to `μ`. Here, "almost everywhere" means except on a set of `μ`-measure zero. This theorem is a variant of `rnDeriv_add`, which doesn't require any condition on `μ`, but needs `ν₁` and `ν₂` to be finite.
More concisely: For three sigma-finite measures `ν₁`, `ν₂`, and `μ` on a measurable space `α`, the Radon-Nikodym derivatives `ν₁ / dμ` and `ν₂ / dμ` almost everywhere exist and are equal almost everywhere to the Radon-Nikodym derivative of `ν₁ + ν₂` with respect to `μ`.
|
MeasureTheory.Measure.measurable_rnDeriv
theorem MeasureTheory.Measure.measurable_rnDeriv :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), Measurable (μ.rnDeriv ν)
This theorem states that for any type `α` with a measurable space `m`, and for any two measures `μ` and `ν` on that measurable space, the Radon-Nikodym derivative of `μ` with respect to `ν` is a measurable function. This means that the preimage of any measurable set under this function is also a measurable set. The Radon-Nikodym derivative provides a way to represent one measure as an integral with respect to another, assuming certain conditions are met.
More concisely: The Radon-Nikodym derivative of two measures on a measurable space is a measurable function.
|
MeasureTheory.Measure.eq_rnDeriv
theorem MeasureTheory.Measure.eq_rnDeriv :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite ν]
{s : MeasureTheory.Measure α} {f : α → ENNReal},
Measurable f → s.MutuallySingular ν → μ = s + ν.withDensity f → ν.ae.EventuallyEq f (μ.rnDeriv ν)
This theorem states that, for any measures 'μ' and 'ν' on a measurable space 'α', if 's' is another measure on 'α' that is mutually singular to 'ν', and 'f' is a measurable function from 'α' to the extended nonnegative real numbers such that 'μ' equals 's' added to 'ν' with density 'f', then almost everywhere with respect to 'ν', the function 'f' equals the Radon-Nikodym derivative of 'μ' with respect to 'ν'. This theorem is crucial to the uniqueness part of the Lebesgue decomposition theorem, asserting the uniqueness of the Radon-Nikodym derivative, complementing another theorem that asserts the uniqueness of the singular part.
More concisely: If measures μ and ν on a measurable space have mutually singular densities f for each other, then almost everywhere with respect to ν, f is the Radon-Nikodym derivative of μ with respect to ν.
|
MeasureTheory.Measure.eq_rnDeriv₀
theorem MeasureTheory.Measure.eq_rnDeriv₀ :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite ν]
{s : MeasureTheory.Measure α} {f : α → ENNReal},
AEMeasurable f ν → s.MutuallySingular ν → μ = s + ν.withDensity f → ν.ae.EventuallyEq f (μ.rnDeriv ν)
This theorem states that, for any measurable space `α`, measures `μ`, `ν` and `s` on `α`, and a function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), under the conditions that `ν` is sigma finite, `f` is almost everywhere measurable with respect to `ν`, and `s` and `ν` are mutually singular (i.e., `s` and `ν` are measures such that there exists a measurable set on which one measure is zero while the other one is zero on the set's complement), then if `μ` equals the sum of `s` and the measure derived from `ν` with density `f`, it must be the case that `f` is almost everywhere equal to the Radon-Nikodym derivative of `μ` with respect to `ν`. In other words, `f` can be thought of as the derivation of `μ` from `ν` when taking into account the mutually singular part `s`.
More concisely: If `μ` is the sum of a sigma-finite measure `ν`, a mutually singular measure `s`, and the product of `ν` and the almost everywhere defined, measurable function `f`, then `f` is the Radon-Nikodym derivative of `μ` with respect to `ν`.
|
MeasureTheory.Measure.eq_singularPart
theorem MeasureTheory.Measure.eq_singularPart :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν s : MeasureTheory.Measure α} {f : α → ENNReal},
Measurable f → s.MutuallySingular ν → μ = s + ν.withDensity f → s = μ.singularPart ν
The theorem `MeasureTheory.Measure.eq_singularPart` states that for any measurable space `α` and measures `μ`, `ν`, and `s` on `α`, and a measurable function `f` from `α` to the extended nonnegative real numbers, if `s` is a measure mutually singular to `ν` and `μ` is the sum of `s` and `ν` multiplied by the density of `f`, then `s` is the singular part of `μ` with respect to `ν`. This theorem basically guarantees the uniqueness of the `singularPart` in the Lebesgue decomposition theorem, with the uniqueness of the `rnDeriv` or Radon-Nikodym derivative provided by the theorem `MeasureTheory.Measure.eq_rnDeriv`.
More concisely: Given a measurable space with measures μ, ν, and s, and a measurable function f: α → [0, ∞], if s is the singular part of μ with respect to ν and μ = s + ν * f's density, then s is the unique singular part of μ with respect to ν.
|
MeasureTheory.Measure.singularPart_le
theorem MeasureTheory.Measure.singularPart_le :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), μ.singularPart ν ≤ μ
This theorem states that for any type `α` and any measurable space `m` on `α`, the singular part of a measure `μ` with respect to another measure `ν` is always less than or equal to `μ`. Here, the singular part of a measure is a concept from measure theory, which intuitively captures the part of a measure that is 'unaccounted for' by another measure.
More concisely: For any measurable spaces `α` and measures `μ` and `ν` on `α`, the singular part of `μ` with respect to `ν` is less than or equal to `μ`.
|
MeasureTheory.Measure.eq_withDensity_rnDeriv
theorem MeasureTheory.Measure.eq_withDensity_rnDeriv :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν s : MeasureTheory.Measure α} {f : α → ENNReal},
Measurable f → s.MutuallySingular ν → μ = s + ν.withDensity f → ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
This theorem states that given measurable spaces `α` and a set of measures `μ`, `ν`, and `s` on `α`, together with a measurable function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), if `s` is mutually singular with `ν` and `μ` is equal to the sum of `s` and the measure `ν` with the density of `f`, then the measure `ν` with the density of `f` is equal to the measure `ν` with the density of the Radon-Nikodym derivative of `μ` with respect to `ν`.
In the context of the Lebesgue decomposition theorem, this theorem ensures the uniqueness of the Radon-Nikodym derivative (`rnDeriv`). While the `MeasureTheory.Measure.eq_singularPart` theorem provides the uniqueness of the `singularPart`, this theorem provides uniqueness in terms of the measures. The uniqueness in terms of the functions is given in `eq_rnDeriv`.
More concisely: If `μ` is the sum of `s` and the measure `ν` with the density of `f`, and `s` is mutually singular with `ν`, then the measures `ν` with densities `f` and the Radon-Nikodym derivative of `μ` with respect to `ν` are equal.
|
MeasureTheory.Measure.rnDeriv_restrict_self
theorem MeasureTheory.Measure.rnDeriv_restrict_self :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite ν]
{s : Set α}, MeasurableSet s → ν.ae.EventuallyEq ((ν.restrict s).rnDeriv ν) (s.indicator 1)
This theorem states that for any measurable space `α`, given a sigma-finite measure `ν` on `α` and a set `s` in `α` that is measurable, the Radon-Nikodym derivative of the restriction of `ν` to `s` is almost everywhere equal to the indicator function of `s`. In other words, the Radon-Nikodym derivative, which essentially quantifies the rate at which one measure changes with respect to another, of the restricted measure is equivalent to the function that is `1` on the set `s` and `0` otherwise, except possibly on a set of measure zero.
More concisely: Let `ν` be a sigma-finite measure on a measurable space `α`, and let `s` be a measurable subset of `α`. Then the Radon-Nikodym derivative of `ν` restricted to `s` is almost everywhere equal to the indicator function of `s`.
|
MeasureTheory.Measure.rnDeriv_withDensity₀
theorem MeasureTheory.Measure.rnDeriv_withDensity₀ :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite ν]
{f : α → ENNReal}, AEMeasurable f ν → ν.ae.EventuallyEq ((ν.withDensity f).rnDeriv ν) f
The theorem `MeasureTheory.Measure.rnDeriv_withDensity₀` states that for any given measurable space (denoted as `α`), and a sigma-finite measure (denoted as `ν`) on it, if a function `f` from this space to the extended nonnegative real numbers (`ENNReal`) is almost everywhere measurable with respect to the measure `ν`, then the Radon-Nikodym derivative of the measure obtained by scaling `ν` with `f` with respect to `ν` is equal to `f` itself almost everywhere.
In other words, if `f` is a function that is measurable almost everywhere and `ν` is a sigma-finite measure, then `f` is its own Radon-Nikodym derivative when used to scale `ν`. The Radon-Nikodym derivative is a concept in measure theory that describes how one measure changes with respect to another and in this case, it's stating that the change in the measure `ν` when scaled by `f` is just `f` itself almost everywhere.
More concisely: If `ν` is a sigma-finite measure on measurable space `α` and `f` is an almost everywhere measurable function from `α` to the extended nonnegative real numbers, then `f` is the Radon-Nikodym derivative of the measure obtained by scaling `ν` with `f` with respect to `ν`.
|
MeasureTheory.Measure.singularPart_def
theorem MeasureTheory.Measure.singularPart_def :
∀ {α : Type u_3} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
μ.singularPart ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).1 else 0
This theorem, `MeasureTheory.Measure.singularPart_def`, in the Measure Theory context, states that for any given measurable space `α` and any two measures `μ` and `ν` on this space, the singular part of `μ` with respect to `ν` is defined as follows: If `μ` and `ν` have a Lebesgue decomposition, then the singular part is the first component of a pair chosen from an indefinite description (existence proof), otherwise, if there's no such decomposition, the singular part is simply zero.
More concisely: The singular part of measure `μ` with respect to `ν` in the measurable space `α` is the first component of their Lebesgue decomposition if it exists, or zero otherwise.
|
MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top'
theorem MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top' :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite ν]
[inst : MeasureTheory.SigmaFinite μ] {r : ENNReal},
r ≠ ⊤ → μ.ae.EventuallyEq ((r • ν).rnDeriv μ) (r • ν.rnDeriv μ)
The theorem `MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top'` states that for any measurable space `α`, and for any two sigma-finite measures `ν` and `μ` on this space, if `r` is a scalar from the extended nonnegative real numbers (which is not infinity), then almost everywhere the Radon-Nikodym derivative of the scalar multiple `r` of `ν` with respect to `μ` is the same as the scalar multiple of the Radon-Nikodym derivative of `ν` with respect to `μ`. This theorem is a version of the well-known property of Radon-Nikodym derivatives under scalar multiplication, but with special considerations for the case where the scalar is an extended nonnegative real number.
More concisely: For any measurable spaces α, sigma-finite measures ν and μ on α, and scalar r from the extended nonnegative real numbers, almost everywhere, the Radon-Nikodym derivative of rν with respect to μ equals r times the Radon-Nikodym derivative of ν with respect to μ.
|
MeasureTheory.Measure.rnDeriv_smul_right
theorem MeasureTheory.Measure.rnDeriv_smul_right :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν]
[inst : ν.HaveLebesgueDecomposition μ] {r : NNReal},
r ≠ 0 → μ.ae.EventuallyEq (ν.rnDeriv (r • μ)) (r⁻¹ • ν.rnDeriv μ)
The theorem `MeasureTheory.Measure.rnDeriv_smul_right` states that for any non-zero nonnegative real number `r`, the Radon-Nikodym derivative of a measure `ν` with respect to a scaled measure `r • μ` (where `μ` is another measure and `•` denotes scalar multiplication) is almost everywhere equal to the scaled Radon-Nikodym derivative `r⁻¹ • ν.rnDeriv μ`. This theorem applies in a measurable space `α` where `μ` and `ν` are measures, `ν` is a finite measure, and `ν` has a Lebesgue decomposition with respect to `μ`.
More concisely: For a finite measure `ν` with a Lebesgue decomposition on measurable space `α` with respect to another measure `μ`, the Radon-Nikodym derivative of `ν` with respect to the scaled measure `r • μ` is almost everywhere equal to `r⁻¹` times the Radon-Nikodym derivative of `ν` with respect to `μ`.
|
MeasureTheory.Measure.rnDeriv_add
theorem MeasureTheory.Measure.rnDeriv_add :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν₁ ν₂ μ : MeasureTheory.Measure α)
[inst : MeasureTheory.IsFiniteMeasure ν₁] [inst : MeasureTheory.IsFiniteMeasure ν₂]
[inst : ν₁.HaveLebesgueDecomposition μ] [inst : ν₂.HaveLebesgueDecomposition μ]
[inst : (ν₁ + ν₂).HaveLebesgueDecomposition μ],
μ.ae.EventuallyEq ((ν₁ + ν₂).rnDeriv μ) (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
This theorem, named `MeasureTheory.Measure.rnDeriv_add`, states that for any measurable space `α` and three measures `ν₁`, `ν₂`, and `μ` defined on this space, if `ν₁` and `ν₂` are finite measures and each of them, as well as their sum, have a Lebesgue decomposition with respect to `μ`, then almost everywhere with respect to `μ`, the Radon-Nikodym derivative of the sum of `ν₁` and `ν₂` with respect to `μ` is equal to the sum of the Radon-Nikodym derivatives of `ν₁` and `ν₂` with respect to `μ`. In mathematical terms, if $d\nu_{1}/d\mu$ and $d\nu_{2}/d\mu$ exist, then $d(\nu_{1}+\nu_{2})/d\mu = d\nu_{1}/d\mu + d\nu_{2}/d\mu$ almost everywhere.
More concisely: If `ν₁` and `ν₂` are finite measures on measurable space `α` with Lebesgue decompositions with respect to `μ`, then almost everywhere, `d(ν₁ + ν₂)/dμ = dν₁/dμ + dν₂/dμ`.
|
MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top'
theorem MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top' :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite ν]
[inst : MeasureTheory.SigmaFinite μ] {r : ENNReal},
r ≠ 0 → r ≠ ⊤ → μ.ae.EventuallyEq (ν.rnDeriv (r • μ)) (r⁻¹ • ν.rnDeriv μ)
The theorem `MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top'` asserts that, for any measurable space `α` and any two sigma-finite measures `ν` and `μ` over this space, if `r` is a non-zero and non-infinite extended nonnegative real number (`ENNReal`), then the Radon-Nikodym derivative of `ν` with respect to the scalar multiple `r` times `μ` is almost everywhere equivalent to `r` inverse times the Radon-Nikodym derivative of `ν` with respect to `μ`. The concept of "almost everywhere" means that the equality holds except possibly on a subset of `α` with measure zero.
More concisely: For measurable spaces `α`, sigma-finite measures `ν` and `μ` over `α`, and a non-zero, non-infinite `r` in the extended nonnegative reals, `ν / r ��ailable μ` is almost everywhere equivalent to `r ∘ ν / μ` where `��ailable` denotes the Radon-Nikodym derivative.
|
MeasureTheory.Measure.rnDeriv_withDensity
theorem MeasureTheory.Measure.rnDeriv_withDensity :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite ν]
{f : α → ENNReal}, Measurable f → ν.ae.EventuallyEq ((ν.withDensity f).rnDeriv ν) f
The theorem `MeasureTheory.Measure.rnDeriv_withDensity` states that for any measurable space `α`, given a sigma-finite measure `ν` on `α` and a measurable function `f` from `α` to the extended nonnegative real numbers (ENNReal, which includes all nonnegative real numbers plus ∞), the Radon-Nikodym derivative of `f ν` (the measure obtained by applying `f` to `ν`) with respect to `ν` is almost everywhere equal to `f`. In other words, except on a set of measure zero, the derivative of the measure `f ν` with respect to the measure `ν` is the function `f` itself.
More concisely: For any measurable space `α`, sigma-finite measure `ν` on `α`, and measurable function `f` from `α` to the extended nonnegative real numbers, the Radon-Nikodym derivative of `f ν` with respect to `ν` equals `f` almost everywhere.
|
MeasureTheory.Measure.rnDeriv_smul_right'
theorem MeasureTheory.Measure.rnDeriv_smul_right' :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite ν]
[inst : MeasureTheory.SigmaFinite μ] {r : NNReal},
r ≠ 0 → μ.ae.EventuallyEq (ν.rnDeriv (r • μ)) (r⁻¹ • ν.rnDeriv μ)
The theorem `MeasureTheory.Measure.rnDeriv_smul_right'` states that for any measure space `α` with a measurable set `m`, given two sigma-finite measures `ν` and `μ` on that space, and a nonzero nonnegative real number `r`, the Radon-Nikodym derivative of `ν` with respect to the scalar multiple of `μ` by `r` is almost everywhere equal to the scalar multiple of the Radon-Nikodym derivative of `ν` with respect to `μ` by the reciprocal of `r`. In simpler terms, it talks about the property of the Radon-Nikodym derivative under scalar multiplication of the measure.
More concisely: For measurable sets m in a sigma-finite measure space α, and sigma-finite measures ν and μ, if ν is absolutely continuous with respect to μ, then the Radon-Nikodym derivative of ν with respect to μ multiplied by a nonzero real number r is almost everywhere equal to the Radon-Nikodym derivative of ν with respect to the scalar multiple of μ by r.
|
MeasureTheory.Measure.haveLebesgueDecomposition_spec
theorem MeasureTheory.Measure.haveLebesgueDecomposition_spec :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [h : μ.HaveLebesgueDecomposition ν],
Measurable (μ.rnDeriv ν) ∧
(μ.singularPart ν).MutuallySingular ν ∧ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
The theorem `MeasureTheory.Measure.haveLebesgueDecomposition_spec` states that for any types `α`, given a measurable space `m` and two measures `μ` and `ν` on that space with the Lebesgue decomposition property, the Radon-Nikodym derivative of `μ` with respect to `ν` is measurable. Furthermore, the singular part of `μ` with respect to `ν` and `ν` themselves are mutually singular. Lastly, `μ` is equal to the sum of its singular part with respect to `ν` and `ν` with the density of the Radon-Nikodym derivative of `μ` with respect to `ν`. In mathematical terms, if `μ` and `ν` are measures with the Lebesgue decomposition property, then `μ = μ_singular + ν * (dμ/dν)`, where `μ_singular` and `ν` are mutually singular, and `dμ/dν` is the Radon-Nikodym derivative of `μ` with respect to `ν`, which is measurable.
More concisely: Given measurable spaces `(α, Σ, m)` and measures `μ` and `ν` on `α` with the Lebesgue decomposition property, the Radon-Nikodym derivative `dμ/dν` of `μ` with respect to `ν` is measurable, and `μ` is equal to the sum of its singular part `μ_singular` with respect to `ν` and `ν` with the product of `ν` and the Radon-Nikodym derivative `dμ/dν`. That is, `μ = μ_singular + ν * (dμ/dν)`, where `μ_singular` and `ν` are mutually singular.
|
MeasureTheory.Measure.rnDeriv_lt_top
theorem MeasureTheory.Measure.rnDeriv_lt_top :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ],
∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ⊤
This theorem states that the Radon-Nikodym derivative of a sigma-finite measure `μ` with respect to another measure `ν` is almost everywhere finite with respect to `ν`. Here, 'almost everywhere' means except on a set of `ν`-measure zero. The theorem is applicable for any measurable space `α` and any sigma-finite measure `μ` on this space. The Radon-Nikodym derivative is a concept from measure theory that expresses the change of one measure with respect to another. The result that it is almost everywhere finite under these conditions is a foundational result in measure theory.
More concisely: In measure theory, for any sigma-finite measure `μ` on a measurable space `α`, the Radon-Nikodym derivative of `μ` with respect to another measure `ν` is almost everywhere finite with respect to `ν`.
|
MeasureTheory.Measure.haveLebesgueDecomposition_add
theorem MeasureTheory.Measure.haveLebesgueDecomposition_add :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : μ.HaveLebesgueDecomposition ν],
μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
This theorem states that for any type `α` and measurable space `m` defined on `α`, given any two measures `μ` and `ν` on this space, if `μ` has a Lebesgue decomposition with respect to `ν`, then `μ` can be represented as the sum of the singular part of `μ` with respect to `ν` and `ν` with the density of the Radon-Nikodym derivative of `μ` with respect to `ν`. In mathematical terms, this is the statement of the Lebesgue Decomposition Theorem which says for any two σ-finite measure spaces, the first measure can be decomposed into the sum of the absolutely continuous part and the singular part with respect to the second measure.
More concisely: Given any two σ-finite measures `μ` and `ν` on a measurable space, `μ` has a Lebesgue decomposition with respect to `ν` as the sum of its singular part and the product of `ν` with the Radon-Nikodym derivative of `μ` with respect to `ν`.
|
MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top
theorem MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top :
∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν]
[inst : ν.HaveLebesgueDecomposition μ] {r : ENNReal},
r ≠ ⊤ → μ.ae.EventuallyEq ((r • ν).rnDeriv μ) (r • ν.rnDeriv μ)
This theorem, named `MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top`, states that for any type `α` with a `MeasurableSpace` structure `m`, given two measures `ν` and `μ` on this measurable space, where `ν` is a finite measure and `ν` admits a Lebesgue decomposition with respect to `μ`, and given an extended non-negative real number `r` which is not equal to infinity (`⊤`), then almost everywhere (`μ.ae.EventuallyEq`) the Radon-Nikodym derivative of `r` times `ν` with respect to `μ` equals `r` times the Radon-Nikodym derivative of `ν` with respect to `μ`. In other words, the Radon-Nikodym derivative of a scalar multiple of a measure is equivalent to the scalar multiple of the Radon-Nikodym derivative of the original measure, under the conditions stated above.
More concisely: Given measurable spaces `(α, m)` with finite measure `ν` admitting a Lebesgue decomposition with respect to `μ`, and extended non-negative real number `r ≠ ⊤`, almost everywhere `(μ.ae)`, `r * ν.RadonNikodymDerivative mu = ν.RadonNikodymDerivative mu * r * ν`.
|
MeasureTheory.Measure.haveLebesgueDecomposition_of_finiteMeasure
theorem MeasureTheory.Measure.haveLebesgueDecomposition_of_finiteMeasure :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
[inst : MeasureTheory.IsFiniteMeasure ν], μ.HaveLebesgueDecomposition ν
This theorem states that for any pair of finite measures `μ` and `ν`, there exists a Lebesgue decomposition. In other words, we can find a measure `ξ` and a measurable function `f` such that `ξ` is mutually singular with respect to `ν` and `μ` can be expressed as the sum of `ξ` and the measure derived from `ν` with density `f`. This theorem is not limited to finite measures, as it is also proven for the more general class of σ-finite measures with the theorem `MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite`.
More concisely: Given any two σ-finite measures `μ` and `ν`, there exists a measurable function `f` and a mutually singular measure `ξ` such that `μ = ξ + ν * f`.
|
MeasureTheory.Measure.lintegral_rnDeriv_lt_top
theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ],
∫⁻ (x : α), μ.rnDeriv ν x ∂ν < ⊤
This theorem states that for any type `α` and measurable space `m` on `α`, for any two measures `μ` and `ν` on `α`, if `μ` is a finite measure, then the Lebesgue integral of the Radon-Nikodym derivative of `μ` with respect to `ν` over the entire space `α` is less than infinity. This is essentially saying that the total "weight" of the Radon-Nikodym derivative is finite under the given conditions.
More concisely: For any measurable spaces `(α, Σ)` and measures `μ, ν` on `α` with `μ` finite, the integral of the Radon-Nikodym derivative of `μ` with respect to `ν` over `α` is finite.
|
MeasureTheory.Measure.withDensity_rnDeriv_le
theorem MeasureTheory.Measure.withDensity_rnDeriv_le :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), ν.withDensity (μ.rnDeriv ν) ≤ μ := by
sorry
This theorem states that for any measurable space `α` and any two measures `μ` and `ν` on that space, the measure formed by weighting `ν` with the Radon-Nikodym derivative of `μ` with respect to `ν` is always less than or equal to `μ`. In mathematical terms, this says that for every measurable set, the integral of the Radon-Nikodym derivative over that set with respect to `ν` is less than or equal to the measure of that set under `μ`.
More concisely: For any measurable spaces `α`, measures `μ` and `ν` on `α` with `ν` being σ-finite and `μ` absolutely continuous with respect to `ν`, we have $\int\_A d\mu / d\nu \leqslant \mu(A)$ for all measurable sets `A` in `α`.
|
MeasureTheory.Measure.rnDeriv_eq_zero
theorem MeasureTheory.Measure.rnDeriv_eq_zero :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : μ.HaveLebesgueDecomposition ν],
ν.ae.EventuallyEq (μ.rnDeriv ν) 0 ↔ μ.MutuallySingular ν
This theorem states that for any two measures `μ` and `ν` in a measurable space `α`, given that `μ` has a Lebesgue decomposition with respect to `ν`, the Radon-Nikodym derivative of `μ` with respect to `ν` is almost everywhere equal to zero if and only if `μ` and `ν` are mutually singular. In other words, `μ` and `ν` are mutually singular if there exists a measurable set such that `μ` gives it measure zero and `ν` gives its complement measure zero, and this is equivalent to the condition that the "rate of change" of `μ` with respect to `ν`, as measured by the Radon-Nikodym derivative, is zero almost everywhere.
More concisely: A measure `μ` is mutually singular with respect to another measure `ν` in a measurable space if and only if the Radon-Nikodym derivative of `μ` with respect to `ν` is almost everywhere equal to zero.
|
MeasureTheory.Measure.mutuallySingular_singularPart
theorem MeasureTheory.Measure.mutuallySingular_singularPart :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), (μ.singularPart ν).MutuallySingular ν
This theorem states that for any measurable space `α` and any two measures `μ` and `ν` on this space, the singular part of `μ` with respect to `ν` is mutually singular with `ν`. In other words, there exists a measurable set `s` such that the singular part of `μ` with respect to `ν` gives zero measure to the set `s`, and `ν` gives zero measure to the complement of `s`.
More concisely: For any measurable spaces `α` and measurable sets `A` on `α`, the singular part of measures `μ` and `ν` on `α` are mutually singular, i.e., there exists a measurable set `s` such that both `μ(s) = 0` and `ν(α \ s) = 0`.
|