MeasureTheory.withDensity_add_left
theorem MeasureTheory.withDensity_add_left :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
Measurable f → ∀ (g : α → ENNReal), μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g
The theorem `MeasureTheory.withDensity_add_left` states that for any type `α` equipped with a measurable space structure `m0` and a measure `μ` defined on that space, for any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`) that is measurable, the measure `μ` with density `f + g` (where `g` is any function from `α` to `ENNReal`) is equal to the sum of the measure `μ` with density `f` and the measure `μ` with density `g`. In other words, the measure with the density of a sum of two functions is equal to the sum of measures with the densities of the individual functions, assuming that the function used in the former is measurable.
More concisely: For any measurable function `f : α → ℝ∞±` and measurable sets `μ` on a measurable space `(α, m0)`, the measure `μ` with density `f + g` equals the sum of the measures `μ` with densities `f` and `g`, where `g : α → ℝ∞±` is any measurable function.
|
MeasureTheory.isFiniteMeasure_withDensity
theorem MeasureTheory.isFiniteMeasure_withDensity :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
∫⁻ (a : α), f a ∂μ ≠ ⊤ → MeasureTheory.IsFiniteMeasure (μ.withDensity f)
The theorem `MeasureTheory.isFiniteMeasure_withDensity` states that for any type `α`, any measurable space `m0` on `α`, any measure `μ` on this measurable space, and any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), if the integral from minus infinity to infinity of `f(a)` with respect to `μ` is not equal to infinity, then the measure `μ` with density `f` is a finite measure. In simpler terms, if the total "weight" assigned by `f` to the elements in `α` under the measure `μ` is finite, then the measure `μ` when "reweighted" by `f` is also finite.
More concisely: If a measurable function `f` from a measurable space `(α, m0)` to the extended nonnegative real numbers has finite integral with respect to a measure `μ` on `α`, then the measure `μ` with density `f` is a finite measure.
|
MeasureTheory.withDensity_apply'
theorem MeasureTheory.withDensity_apply' :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ]
(f : α → ENNReal) (s : Set α), ↑↑(μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ
The theorem `MeasureTheory.withDensity_apply'` states that, for any type `α`, any measurable space `m0` on `α`, any measure `μ` on `α` that is sigma-finite, any function `f` from `α` to the extended nonnegative real numbers, and any set `s` of `α`, the measure of `s` with respect to the measure `μ` "weighted" by `f` (denoted `μ.withDensity f`) is equal to the integral over `s` of `f` with respect to `μ`. In mathematical terms, `∫⁻ (a : α) in s, f a ∂μ` represents the Lebesgue integral of the function `f` over the set `s` with respect to the measure `μ`.
More concisely: For any sigma-finite measure `μ` on a measurable space `(α, m0)` and measurable function `f` from `α` to the extended nonnegative reals, the integral of `f` with respect to `μ` equals the measure of the set where `f` is positive, weighted by `f` itself, according to `μ.withDensity f`.
|
MeasureTheory.restrict_withDensity
theorem MeasureTheory.restrict_withDensity :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasurableSet s → ∀ (f : α → ENNReal), (μ.withDensity f).restrict s = (μ.restrict s).withDensity f
The theorem `MeasureTheory.restrict_withDensity` states that for any given type `α`, a measurable space `m0` on `α`, a measure `μ` on `α`, and a set `s` of type `α`, if `s` is a measurable set, then for any function `f` mapping elements of `α` to extended nonnegative real numbers (`ENNReal`), the measure of `s` obtained by first applying `withDensity f` to `μ` and then restricting to `s` is equal to the measure obtained by first restricting `μ` to `s` and then applying `withDensity f`. In other words, the sequence of applying `withDensity` and `restrict` operations on `μ` is commutative. This theorem is related to the properties of a measure when it is transformed by a function and then restricted to a measurable subset, or vice versa.
More concisely: For any measurable space `(α, μ)`, measurable set `s ∈ α`, and function `f: α → ENNReal`, the measures of `s` obtained by first applying `withDensity f` to `μ` and then restricting to `s`, and by first restricting `μ` to `s` and then applying `withDensity f`, are equal.
|
MeasureTheory.ae_withDensity_iff
theorem MeasureTheory.ae_withDensity_iff :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} {f : α → ENNReal},
Measurable f → ((∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x)
This theorem states that for any type `α`, measurable space `m0`, measure `μ`, proposition `p` and function `f` from `α` to the extended nonnegative reals, if `f` is measurable, then the property `p` holds almost everywhere (in the sense of measure `μ`) with respect to the measure obtained by applying `f` to `μ` (denoted `μ.withDensity f`), if and only if `p` holds almost everywhere with respect to `μ` whenever `f` is not zero. In other words, the set of points where `p` fails is of measure zero in `μ.withDensity f` if and only if the set of points where both `p` fails and `f` is not zero is of measure zero in `μ`.
More concisely: For a measurable function $f : \alpha \to \mathbb{R}^+ \cup \{ \infty \}$ from a type $\alpha$ to the extended nonnegative reals and any measure $\mu$, proposition $p$, if $f$ is measurable and $\mu.withDensity(f) = \mu$ almost everywhere where $f$ is nonzero if and only if $p$ holds almost everywhere with respect to $\mu$, then $p$ holds almost everywhere with respect to $\mu.withDensity(f)$.
|
MeasureTheory.withDensity_absolutelyContinuous'
theorem MeasureTheory.withDensity_absolutelyContinuous' :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
AEMeasurable f μ →
(∀ᵐ (x : α) ∂μ, f x ≠ 0) → (∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → μ.AbsolutelyContinuous (μ.withDensity f)
The theorem `MeasureTheory.withDensity_absolutelyContinuous'` states that for any measurable space `α`, given a measure `μ` on `α` and a function `f : α → ENNReal` (which maps `α` into the extended nonnegative real numbers), if `f` is almost everywhere measurable with respect to `μ`, `f` is almost everywhere nonzero, and `f` is almost everywhere finite (i.e., it does not equal infinity), then `μ` is absolutely continuous with respect to the measure `μ` with density `f`. In converse, the theorem `withDensity_absolutelyContinuous` always holds. In mathematical terms, it says that if a function is almost everywhere positive and finite, then the measure is absolutely continuous with respect to its own measure when the density is defined by this function.
More concisely: If a measurable function `f : α → ENNReal` is almost everywhere non-zero, finite, and measurable with respect to a measure `μ` on `α`, then `μ` is absolutely continuous with respect to `μ` with density `f`.
|
MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀'
theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀' :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
AEMeasurable f μ →
∀ {g : α → ENNReal},
AEMeasurable g (μ.withDensity f) → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
This theorem is about Lebesgue integration in measure theory. It states that for any measure space α, with measurable space m0 and measure μ, if we have a function `f` from α to the extended nonnegative real numbers that is almost everywhere measurable, then for any other function `g` from α to the extended nonnegative real numbers that is almost everywhere measurable with respect to the measure `μ.withDensity f`, the Lebesgue integral of `g` with respect to `μ.withDensity f` is equal to the Lebesgue integral of the product of `f` and `g` with respect to `μ`. This theorem assumes that `g` is almost everywhere measurable. There is another version of this theorem that doesn't require `g` to be almost everywhere measurable but instead needs `f` to be almost everywhere finite, named `lintegral_withDensity_eq_lintegral_mul_non_measurable`.
More concisely: For any measure space α, if `f` and `g` are almost everywhere measurable functions from α to the extended nonnegative real numbers, then the Lebesgue integral of `g` with respect to the measure `μ.withDensity f` is equal to the Lebesgue integral of the product `f * g` with respect to `μ`.
|
MeasureTheory.withDensity_apply_le
theorem MeasureTheory.withDensity_apply_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) (s : Set α),
∫⁻ (a : α) in s, f a ∂μ ≤ ↑↑(μ.withDensity f) s
This theorem, `MeasureTheory.withDensity_apply_le`, in the field of Measure Theory, states that for any given type α, a measurable space `m0` on α, a measure `μ` on that measurable space, a function `f` from α to the extended nonnegative real numbers (usually denoted [0, ∞]), and a set `s` of type α, the Lebesgue integral (or the 'proper' integral) over the set `s` of the function `f` with respect to the measure `μ` is less than or equal to the measure of the set `s` with respect to the density of the measure `μ` as defined by the function `f`. In other words, the total 'amount of stuff' as measured by the function `f` over the set `s` is less than or equal to the total measure of the set `s` when we consider the measure `μ` to have been 'adjusted' by the function `f`.
More concisely: For any measurable space (α, m0), measure μ, measurable function f : α → [0, ∞], and set s ∈ m0, we have ∫(s) (f) dμ ≤ μ(s).
|
MeasureTheory.withDensity_absolutelyContinuous
theorem MeasureTheory.withDensity_absolutelyContinuous :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
(μ.withDensity f).AbsolutelyContinuous μ
The theorem `MeasureTheory.withDensity_absolutelyContinuous` states that for any measure μ and any function f from a type α to the extended nonnegative real numbers (ENNReal), the measure with density f with respect to the measure μ is absolutely continuous with respect to μ. In mathematical terms, this means that if for any set A, if the measure μ assigns it a measure of 0, then the measure with density f also assigns it a measure of 0. This property is important in measure theory and probability theory because it relates the behavior of the original measure μ and the derived measure with density f.
More concisely: If `μ` is a measure and `f : α → ↑ℝ` is a function, then the measure with density `f` with respect to `μ` is absolutely continuous with respect to `μ`.
|
MeasureTheory.withDensity_indicator
theorem MeasureTheory.withDensity_indicator :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasurableSet s → ∀ (f : α → ENNReal), μ.withDensity (s.indicator f) = (μ.restrict s).withDensity f
The theorem `MeasureTheory.withDensity_indicator` states that for any measurable space `α`, a measure `μ` on that space, and a set `s` in that space, if the set `s` is measurable, then for any function `f` mapping from `α` to the extended nonnegative real numbers, the measure with density defined by the set indicator function of `s` and `f` is equal to the measure restricted to `s` with density `f`. In simpler terms, considering only the measure on the set `s` and ignoring the rest of the space doesn't change the density calculation.
More concisely: For any measurable space, measure, set, and function, the measure with density defined by the set indicator function of a measurable set and the given function is equal to the measure restricted to that set with the same density function.
|
MeasureTheory.withDensity_congr_ae
theorem MeasureTheory.withDensity_congr_ae :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
μ.ae.EventuallyEq f g → μ.withDensity f = μ.withDensity g
The theorem `MeasureTheory.withDensity_congr_ae` states that for any type `α`, any `MeasurableSpace α` named `m0`, any measure `μ` over that space, and any two functions `f` and `g` from `α` to the extended nonnegative real numbers, if `f` is equal to `g` almost everywhere with respect to the measure `μ` (expressed as `f =ᶠ[MeasureTheory.Measure.ae μ] g`), then the measure `μ` with the density function `f` is equal to the measure `μ` with the density function `g` (expressed as `μ.withDensity f = μ.withDensity g`). This theorem is particularly useful when working with measure theory, as it allows us to equate two measures if their density functions are equal almost everywhere.
More concisely: If two functions have the same density with respect to a measure almost everywhere, then the measures with these densities are equal.
|
MeasureTheory.withDensity_smul
theorem MeasureTheory.withDensity_smul :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal},
Measurable f → μ.withDensity (r • f) = r • μ.withDensity f
This theorem states that for any measurable space `α`, equipped with a measure `μ`, and for any extended nonnegative real number `r` and any function `f` from `α` to the extended nonnegative real numbers that is measurable, the measure with density of `r` scaled by `f` is equal to `r` scaled by the measure with density `f`. In mathematical terms, if `f : α → [0, ∞]` is a measurable function on a measurable space `α` with a measure `μ`, then the measure with density `r*f` is the same as `r` times the measure with density `f`, where `r` is in `[0, ∞]`.
More concisely: For any measurable space `α` with measure `μ`, and measurable function `f : α → [0, ∞]` on `α`, the measure with density `r * f` is equal to `r` times the measure with density `f` for any extended nonnegative real number `r`.
|
MeasureTheory.withDensity_one
theorem MeasureTheory.withDensity_one :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.withDensity 1 = μ
This theorem states that for any type `α`, any measurable space `α` is equipped with `m0`, and any measure `μ` of type `MeasureTheory.Measure α`, applying the `withDensity` function to `μ` with the constant function `1` returns `μ` itself. Essentially, the measure with density 1 is the same as the original measure, in the context of Measure Theory.
More concisely: For any measurable space `(α, Σ)` and measure `μ : MeasureTheory.Measure α`, `μ` equals `withDensity 1 μ`.
|
MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀
theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀ :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} {s : Set α},
AEMeasurable f (μ.restrict s) →
∀ (g : α → ENNReal),
MeasurableSet s →
(∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤) →
∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
The theorem `MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀` states that for any type `α` with a measurable space structure `m0`, a measure `μ` on `α`, a function `f` from `α` to the extended nonnegative real numbers, and a set `s` of type `α`, if `f` is almost everywhere measurable with respect to the restriction of `μ` to `s`, then for any function `g` from `α` to the extended nonnegative real numbers, if `s` is a measurable set and `f` is finite almost everywhere with respect to the restriction of `μ` to `s`, the Lebesgue integral over `s` with respect to the measure `μ` with density `f` of `g` is equal to the Lebesgue integral over `s` with respect to `μ` of the product of `f` and `g`. In mathematical notation, this can be written as:
$$
\int_{s} g \, d(\mu \, dx) = \int_{s} (f \, g) \, d\mu
$$
where the integral is the Lebesgue integral, `f` is almost everywhere finite and measurable, `g` is any function from `α` to the extended nonnegative real numbers, `s` is a measurable set, and `μ` is a measure on `α`.
More concisely: For a measurable space `(α, m0)`, measure `μ`, almost everywhere finite and measurable function `f`, measurable set `s`, and functions `g` and `h = f * g`, the Lebesgue integrals of `g` and `h` with respect to `μ` over `s` are equal: `∫s g dμ = ∫s h dμ`.
|
MeasureTheory.withDensity_mul₀
theorem MeasureTheory.withDensity_mul₀ :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
AEMeasurable f μ → AEMeasurable g μ → μ.withDensity (f * g) = (μ.withDensity f).withDensity g
This theorem states that for any type `α`, given a measurable space `m0` of `α`, a measure `μ` on the measurable space, and two functions `f` and `g` mapping from `α` to the extended nonnegative real numbers (usually denoted [0, ∞]), if `f` and `g` are almost everywhere measurable with respect to measure `μ`, then the measure `μ` with density `f * g` is equal to the measure with density `g` derived from the measure `μ` with density `f`. In mathematical terms, it says that for almost every measurable functions `f` and `g`, the measure with density `f * g` is the same as composing the measure with density `f` and then with density `g`.
More concisely: For measurable functions `f` and `g` mapping from a measurable space `(α, m0)` to the extended nonnegative real numbers, if `f` and `g` are almost everywhere equal almost everywhere with respect to measure `μ`, then the measure `μ` with density `f * g` equals the measure obtained by composing the measures with densities `f` and `g`: `μ {| α | f * g} = (μ {| α | f}) {| α | g}`.
|
MeasureTheory.withDensity_zero
theorem MeasureTheory.withDensity_zero :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.withDensity 0 = 0
This theorem states that for any type `α`, any measurable space `m0` over type `α`, and any measure `μ` of the measure theory over `α`, the measure-theoretical density of `μ` with respect to the zero function is equal to the zero measure. In simpler terms, it means that if you calculate the density of any measure with a zero function, the resulting measure will also be zero.
More concisely: For any measure `μ` over measurable space `(α, m0)`, the density of `μ` with respect to the zero measure is zero.
|
MeasureTheory.withDensity_const
theorem MeasureTheory.withDensity_const :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal),
(μ.withDensity fun x => c) = c • μ
The theorem `MeasureTheory.withDensity_const` states that for any type `α`, measurable space `m0` on `α`, measure `μ` on this measurable space, and an extended nonnegative real number `c`, the measure `μ` with density function being a constant function that always returns `c` is equivalent to `c` times the original measure `μ`. In other words, if we "weight" all elements of the measurable space uniformly by a factor of `c`, this is the same as scaling the entire measure by `c`.
More concisely: For any measurable space `(α, m0)`, measure `μ`, and constant function `c : ℝ≥0∞`, `μ` is equivalent to `c * μ` when `c` is the density function of `μ`.
|
MeasureTheory.withDensity_apply
theorem MeasureTheory.withDensity_apply :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {s : Set α},
MeasurableSet s → ↑↑(μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ
The theorem `MeasureTheory.withDensity_apply` states that for any type `α`, any measurable space `m0` on `α`, any measure `μ` on `α`, any function `f` from `α` to the extended nonnegative real numbers, and any set `s` of type `α`, if `s` is a measurable set, then the double coercion of the measure of `s` with density `f` is equal to the integral over `s` with respect to `μ` of the function `f`. In other words, this theorem relates the concept of a measure with density to the concept of an integral over a measurable set.
More concisely: For any measurable space `(α, m0)`, measure `μ`, function `f` to extended nonnegative real numbers, and measurable set `s`, the double coercion of `μ s` with density `f` equals the integral of `f` over `s` with respect to `μ`.
|
MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure
theorem MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ],
∃ ν, MeasureTheory.IsFiniteMeasure ν ∧ μ.AbsolutelyContinuous ν
This theorem states that for any sigma-finite measure (a measure for which the entire space can be decomposed into a countable union of sets each of which has finite measure), there exists a finite measure with respect to which the sigma-finite measure is absolutely continuous. In other words, if for every subset of the space, the finite measure of the subset is zero, then the sigma-finite measure of the subset is also zero. The theorem is applicable in any measurable space, and the measures can be applied to any type of elements in the space.
More concisely: Every sigma-finite measure has an absolutely continuous finite measure representative.
|
MeasureTheory.lintegral_withDensity_eq_lintegral_mul
theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
Measurable f → ∀ {g : α → ENNReal}, Measurable g → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
This theorem, Exercise 1.2.1 from [tao2010], relates to the integration of a measurable function with respect to a measure, specifically the measure `(μ.withDensity f)`. It states that for any given measure `μ`, often the Lebesgue measure, and any given measurable functions `f` and `g`, the integral with respect to `(μ.withDensity f)` of `g` is equal to the integral with respect to `μ` of the product of `f` and `g`. This is particularly relevant when `f` represents a probability density function and `(μ.withDensity f)` represents a continuous random variable as a probability measure, such as various standard distributions (uniform, Gaussian, exponential, Beta, Cauchy). Hence, this theorem provides a method for calculating expectations, variances, and other statistical moments as a function of the probability density function.
More concisely: For any measurable functions `f` and `g` and measure `μ`, the integral of `g` with respect to the measure `(μ.withDensity f)` equals the integral of the product of `f` and `g` with respect to `μ`.
|