MeasureTheory.withDensity_eq_iff_of_sigmaFinite
theorem MeasureTheory.withDensity_eq_iff_of_sigmaFinite :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite μ]
{f g : α → ENNReal},
AEMeasurable f μ → AEMeasurable g μ → (μ.withDensity f = μ.withDensity g ↔ μ.ae.EventuallyEq f g)
The theorem `MeasureTheory.withDensity_eq_iff_of_sigmaFinite` states that for any measure space `α` with a sigma-finite measure `μ`, and any two functions `f` and `g` from `α` to the extended nonnegative real numbers (`ENNReal`), if `f` and `g` are both almost everywhere measurable (i.e., each coincides almost everywhere with a measurable function), then the measure `μ` with density `f` is equal to the measure `μ` with density `g` if and only if `f` is equal to `g` almost everywhere with respect to the measure `μ`. In other words, two almost everywhere measurable functions contribute the same density to a sigma-finite measure if and only if they are equal almost everywhere.
More concisely: For any sigma-finite measure space `α` and almost everywhere measurable functions `f` and `g` from `α` to the extended nonnegative real numbers, `μ{f} = μ{g}` if and only if `f = g` almost everywhere with respect to `μ`.
|
MeasureTheory.ae_le_of_forall_set_lintegral_le_of_sigmaFinite
theorem MeasureTheory.ae_le_of_forall_set_lintegral_le_of_sigmaFinite :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite μ]
{f g : α → ENNReal},
Measurable f →
Measurable g →
(∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ) →
μ.ae.EventuallyLE f g
The theorem `MeasureTheory.ae_le_of_forall_set_lintegral_le_of_sigmaFinite` states that for any type `α` with a measurable space `m0` and a sigma-finite measure `μ`, given two functions `f` and `g` from `α` to the extended non-negative reals (`ENNReal`), if both `f` and `g` are measurable, and for every measurable set `s` with a measure that's less than infinity, the integral of `f` over `s` with respect to `μ` is less than or equal to the integral of `g` over `s` with respect to `μ`, then `f` is less than or equal to `g` almost everywhere with respect to measure `μ`. This essentially says that if one function's integral is less than or equal to another's over all measurable sets, then the first function is less than or equal to the second almost everywhere.
More concisely: If `α` is a type with a sigma-finite measure `μ`, `f` and `g` are measurable functions from `α` to the extended non-negative reals, and for every measurable set `s` with finite measure, `∫(s, μ, f) ≤ ∫(s, μ, g)`, then `f ≤ g` almost everywhere with respect to `μ`.
|
MeasureTheory.withDensity_eq_iff
theorem MeasureTheory.withDensity_eq_iff :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
AEMeasurable f μ →
AEMeasurable g μ → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → (μ.withDensity f = μ.withDensity g ↔ μ.ae.EventuallyEq f g)
This theorem states that for any measurable space `α`, and any measure `μ` over that space, if `f` and `g` are two functions from `α` to the extended nonnegative real numbers that are almost everywhere measurable with respect to `μ`, and the integral of `f` with respect to `μ` is not infinity, then the measure `μ` with density `f` is equal to the measure `μ` with density `g` if and only if `f` is almost everywhere equal to `g` with respect to the measure `μ`. In simpler terms, it says that two measures with the same almost everywhere measurable density functions are equivalent.
More concisely: For any measurable space `α` and measure `μ`, two almost everywhere measurable functions `f` and `g` from `α` to the extended nonnegative real numbers with finite integral with respect to `μ`, have equivalent measures `μ` with densities `f` and `g` if and only if `f` is almost everywhere equal to `g` with respect to `μ`.
|
MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg_of_stronglyMeasurable
theorem MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg_of_stronglyMeasurable :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
MeasureTheory.StronglyMeasurable f →
MeasureTheory.Integrable f μ →
(∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ) → μ.ae.EventuallyLE 0 f
This theorem, dubbed as an alias of `MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_stronglyMeasurable`, states that for any type `α` with a given measurable space `m0` and a measure `μ`, if a function `f` from `α` to the real numbers is strongly measurable and integrable with respect to `μ`, then if for any set `s` of type `α` that is measurable and has a measure less than infinity, the integral of `f` over `s` is non-negative, it follows that `f` is almost everywhere greater than or equal to zero with respect to the measure `μ`.
The theorem recommends using `ae_nonneg_of_forall_setIntegral_nonneg` instead of itself.
More concisely: If a strongly measurable and integrable real-valued function on a measurable space is non-negative almost everywhere with respect to the measure, then it is almost everywhere greater than or equal to zero.
|
MeasureTheory.ae_eq_zero_of_forall_set_integral_isClosed_eq_zero
theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_isClosed_eq_zero :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {β : Type u_3}
[inst_3 : TopologicalSpace β] [inst_4 : MeasurableSpace β] [inst_5 : BorelSpace β] {μ : MeasureTheory.Measure β}
{f : β → E},
MeasureTheory.Integrable f μ → (∀ (s : Set β), IsClosed s → ∫ (x : β) in s, f x ∂μ = 0) → μ.ae.EventuallyEq f 0
This theorem can be stated as follows:
Given a normed addative commutative group `E` which is also a normed space over the reals with the completeness property, a topological space `β` which is also a measurable space and has Borel sigma algebra, a measure `μ` on `β`, and a function `f` from β to E. If `f` is integrable with respect to `μ` and the integral of `f` over any closed set is zero, then `f` is equal to zero almost everywhere with respect to the measure `μ`.
This is essentially a statement about the "vanishing" of a function under certain measure-theoretic conditions.
More concisely: If a real-valued function on a Borel measurable space with a complete normed additive commutative group valued integrable under a finite measure with the property that the integral over any closed set is zero, then the function is almost everywhere equal to the zero function.
|