MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul
theorem MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} (μ : MeasureTheory.Measure α),
μ.ae.EventuallyLE 0 f →
AEMeasurable f μ →
∀ {p : ℝ},
0 < p →
∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, ↑↑μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
This theorem, known as an application of the layer cake formula, Cavalieri's principle, or tail probability formula, states the following for a measure space:
Given a nonnegative function `f` and a measure `μ` such that `f` is almost everywhere measurable and is almost everywhere less than or equal to 0, for any real number `p` greater than 0, the Lebesgue integral of `f` raised to the `p`-th power can be computed as `p` times the Lebesgue integral over the set of real numbers greater than 0, where the integrand is the measure of the set of elements `a` such that `f(a)` is greater than `t`, multiplied by `t` raised to the power of `p-1`.
In mathematical terms, this is expressed as:
`∫⁻ f^p dμ = p * ∫⁻ t in (0,∞), μ({ω | f(ω) > t}) * t^(p-1)`.
This theorem provides a method for calculating the integral of a function raised to a power, given certain conditions on the function and the power.
More concisely: For a nonnegative, almost everywhere measurable function `f` and measure `μ` such that `f(ω) ≤ 0` almost everywhere, the integral of `f^p` with respect to `μ` equals `p` times the integral of the measure of `{ω | f(ω) > t}` raised to the power of `p-1` multiplied by `t^(p-1)` over `t` in the interval `(0, ∞)`.
|
MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable
theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α),
0 ≤ f →
Measurable f →
(∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
Measurable g →
(∀ t > 0, 0 ≤ g t) →
∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
∫⁻ (t : ℝ) in Set.Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
This theorem formalizes a version of the layer cake formula (also known as Cavalieri's principle or the tail probability formula), but with a measurability assumption that would typically be implied by integrability assumptions. Unlike `lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite`, it does not require a sigma-finite assumption. Here, the theorem asserts that for any measurable space `α`, a nonnegative function `f` from `α` to `ℝ` and another function `g` from `ℝ` to `ℝ` under measure `μ`, if `f` is measurable, `g` is interval integrable over any interval from 0 to any positive `t`, `g` is measurable and nonnegative for any `t > 0`, then the Lebesgue integral of the composition of `ENNReal.ofReal` and the definite integral from 0 to `f ω` of `g` with respect to `μ` is equal to the extended nonnegative real number of the Lebesgue integral over the set of all `t > 0` of the measure of the set of `a` for which `t ≤ f a` times the `ENNReal.ofReal` of `g t`.
More concisely: If `α` is a measurable space, `f: α → ℝ` is measurable, and `g: ℝ → ℝ` is interval integrable and nonnegative for any positive `t`, then the Lebesgue integral of `ENNReal.ofReal ∘ (∫0≤t≤f(a) dt g(t)) dμ(a)` equals the extended nonnegative real number of the Lebesgue integral of `g(t)` over the set `{a ∈ α | t > 0 and t ≤ f(a)}` with respect to the measure `μ`.
|
MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul
theorem MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} (μ : MeasureTheory.Measure α),
μ.ae.EventuallyLE 0 f →
AEMeasurable f μ →
∀ {p : ℝ},
0 < p →
∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
This theorem, which is an application of the layer cake formula, Cavalieri's principle, or the tail probability formula, states the following:
Given a nonnegative function `f` on a measure space with measure `μ` and a positive real number `p`, if `f` is almost everywhere measurable and nonnegative almost everywhere, then the Lebesgue integral of `f` raised to the power of `p` can be expressed as `p` times the integral from 0 to ∞ (exclusive) of `t` raised to the power of `p-1` times the measure of the set of points where `f` is greater than or equal to `t`. Specifically, the theorem is represented as: `∫⁻ f^p ∂μ = p * ∫⁻ t in 0..∞, t^(p-1) * μ {ω | f(ω) ≥ t}`.
The theorem also refers to another version, `MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul`, which has sets of the form `{ω | f(ω) > t}` instead.
More concisely: The Lebesgue integral of a nonnegative, almost everywhere measurable function `f` raised to the power `p` is equal to `p` times the integral of `t` raised to the power `p-1` multiplied by the measure of the set where `f` exceeds `t`.
|
MeasureTheory.meas_le_ae_eq_meas_lt
theorem MeasureTheory.meas_le_ae_eq_meas_lt :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {R : Type u_3} [inst_1 : LinearOrder R]
[inst_2 : MeasurableSpace R] (ν : MeasureTheory.Measure R) [inst_3 : MeasureTheory.NoAtoms ν] (g : α → R),
ν.ae.EventuallyEq (fun t => ↑↑μ {a | t ≤ g a}) fun t => ↑↑μ {a | t < g a}
This theorem states that for any type `α` with a `MeasurableSpace` instance, any measure `μ` on `α`, any type `R` with a `LinearOrder` and `MeasurableSpace` instances, any measure `ν` on `R` where `ν` has no atoms (i.e., each singleton set has measure zero), and any function `g` from `α` to `R`, the measure `μ` of the set of elements `α` such that `t` is less than or equal to `g(a)` is almost everywhere equal (with respect to the measure `ν`) to the measure `μ` of the set of elements `α` such that `t` is less than `g(a)`. In mathematical terms, for almost all `t`, we have `μ({a | t ≤ g a}) = μ({a | t < g a})`.
More concisely: For any measurable space `(α, μ)`, any measurable function `g : α → ℝ` with values in a linearly ordered and measurable space `(ℝ, ν)` having no atoms, and `ν`-almost every `t ∈ ℝ`, we have `μ({a | t ≤ g a}) = μ({a | t < g a})`.
|
MeasureTheory.lintegral_eq_lintegral_meas_lt
theorem MeasureTheory.lintegral_eq_lintegral_meas_lt :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} (μ : MeasureTheory.Measure α),
μ.ae.EventuallyLE 0 f →
AEMeasurable f μ → ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, ↑↑μ {a | t < f a}
This theorem, known as the layer cake formula, Cavalieri's principle, or the tail probability formula, states that for a nonnegative function `f` on a measure space, the Lebesgue integral of `f` can be expressed as the integral over the interval from 0 to infinity of the measure of the set where `f(ω)` is greater than `t`. More formally, if `α` is a type with a measurable space structure, `f` is a function from `α` to real numbers, and `μ` is a measure on `α`, assuming that `f` is almost everywhere measurable and `f` is almost everywhere less than or equal to 0, then the Lebesgue integral of the nonnegative version of `f` with respect to `μ` is equal to the Lebesgue integral over the open interval (0, ∞) of the measure of the set where `f(a)` is greater than `t`. This theorem provides an alternate way to calculate Lebesgue integrals which can be useful in some situations.
More concisely: The Lebesgue integral of a nonnegative, almost everywhere defined function `f` with respect to measure `μ` is equal to the integral over (0, ∞) of the measure of `{x | f(x) > t}`.
|
MeasureTheory.Integrable.integral_eq_integral_meas_lt
theorem MeasureTheory.Integrable.integral_eq_integral_meas_lt :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ},
MeasureTheory.Integrable f μ →
μ.ae.EventuallyLE 0 f → ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioi 0, (↑↑μ {a | t < f a}).toReal
This theorem, known as the standard case of the layer cake formula, Cavalieri's principle, or tail probability formula, states that for an almost everywhere nonnegative real-valued function `f` that is integrable with respect to a measure `μ`, the Bochner integral of `f` can be represented as the integral from 0 to infinity of the measure of the set of points where `f` is greater than `t`. In other words, the integral of `f` with respect to `μ` is equal to the integral over the interval (0, ∞) of the measure of the set of points `a` such that `f(a)` is greater than `t`. A version of this theorem that uses the Lebesgue integral instead of the Bochner integral is also available.
More concisely: The Bochner integral of an almost everywhere nonnegative integrable function `f` with respect to a measure `μ` equals the integral from 0 to infinity of the measure of `{x | f(x) > t}` dt.
|
MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite
theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α)
[inst_1 : MeasureTheory.SigmaFinite μ],
0 ≤ f →
Measurable f →
(∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
Measurable g →
(∀ t > 0, 0 ≤ g t) →
∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
∫⁻ (t : ℝ) in Set.Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
This theorem is an auxiliary version of the layer cake formula, also known as Cavalieri's principle or the tail probability formula. It assumes measurability that would essentially follow from the integrability assumptions and also a sigma-finiteness assumption.
Given a measurable space `α`, a function `f: α → ℝ`, a function `g: ℝ → ℝ`, and a measure `μ` on `α` which is sigma-finite, if `f` is nonnegative and measurable, and `g` is interval integrable over `(0, t]` for any `t > 0`, is measurable, and nonnegative for `t > 0`, then the Lebesgue integral of the composition of `ENNReal.ofReal` and the integral from `0` to `f ω` of `g t` with respect to `μ` is equal to the Lebesgue integral over `(0, +∞)` of the product of the measure `μ` of the set `{a | t ≤ f a}` and `ENNReal.ofReal (g t)`.
More concisely: Given a sigma-finite measure `μ` on a measurable space `α`, a nonnegative measurable function `f: α → ℝ`, and an interval integrable function `g: ℝ → ℝ` for which `f` and `g t` are nonnegative for `t > 0`, the Lebesgue integrals of `ENNReal.ofReal (g (f ω))` with respect to `μ` and of `g t * μ({a | t ≤ f a})` over `(0, +∞)` are equal.
|
MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul
theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α),
μ.ae.EventuallyLE 0 f →
AEMeasurable f μ →
(∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
(∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), 0 ≤ g t) →
∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
∫⁻ (t : ℝ) in Set.Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
This theorem is known as the "layer cake formula", Cavalieri's principle, or the tail probability formula in measure theory. It states that given a measure space and a non-negative measurable function `f` on this space, and an increasing absolutely continuous function `G` on the positive real line that vanishes at the origin with derivative `g = G'`, the integral of the composition `G ∘ f` can be expressed as the integral over the positive real line of the tail measures `μ {ω | f(ω) ≥ t}` of `f` weighted by `g`.
More formally, `∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0..∞, g(t) * μ {ω | f(ω) ≥ t}`. This can be interpreted as the integral of the function `G ∘ f` with respect to the measure `μ` being equal to the integral from 0 to infinity of the measure of the set `{ω | f(ω) ≥ t}` times the value `g(t)`. This theorem requires that the function `f` is almost everywhere measurable, and that for all positive `t`, the function `g` is interval integrable on the interval from 0 to `t`.
Please note that there is a similar version of this theorem which deals with sets of the form `{ω | f(ω) > t}` instead.
More concisely: Given a measure space, a non-negative measurable function `f`, and an increasing Absolutely Continuous function `G` with vanishing origin and interval integrable derivative `g`, the integral of `G ∘ f` with respect to `μ` equals the integral of `g(t) * μ({ω|f(ω) ≥ t})` from 0 to infinity.
|
MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul
theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α),
μ.ae.EventuallyLE 0 f →
AEMeasurable f μ →
(∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
(∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), 0 ≤ g t) →
∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
∫⁻ (t : ℝ) in Set.Ioi 0, ↑↑μ {a | t < f a} * ENNReal.ofReal (g t)
This theorem, also known as the layer cake formula, Cavalieri's principle, or tail probability formula, states the following:
Let `f` be a non-negative measurable function on a measure space, and `G` be an increasing absolutely continuous function on the positive real line that vanishes at the origin, with derivative `G' = g`. Then the integral of the composition `G ∘ f`, can be represented as the integral over the positive real line of the "tail measures" `μ {ω | f(ω) > t}` of `f`, weighted by `g`.
More explicitly, the theorem states that `∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0..∞, g(t) * μ {ω | f(ω) > t}`.
The theorem has a few conditions:
- `f` must be almost everywhere measurable
- `g` must be interval integrable over every interval `(0, t]` for `t > 0`
- Almost everywhere on the interval `(0, ∞)`, `g` must be non-negative.
This theorem also has a variant, `lintegral_comp_eq_lintegral_meas_le_mul`, where the "tail measures" are defined for sets of the form `{ω | f(ω) ≥ t}` instead of `{ω | f(ω) > t}`.
More concisely: Let `f` be a non-negative measurable function and `G` an increasing absolutely continuous function with non-negative derivative `g`, then `∫⁻ (G ∘ f) dμ = ∫⁻ t in 0^∞, g(t) * μ {ω | f(ω) > t} dt`, where `μ` is the measure on the measure space.
|
MeasureTheory.lintegral_eq_lintegral_meas_le
theorem MeasureTheory.lintegral_eq_lintegral_meas_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} (μ : MeasureTheory.Measure α),
μ.ae.EventuallyLE 0 f →
AEMeasurable f μ → ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, ↑↑μ {a | t ≤ f a}
The theorem `MeasureTheory.lintegral_eq_lintegral_meas_le` states that for any measure space `α` and any nonnegative function `f` from `α` to real numbers, provided `f` is almost everywhere measurable with respect to a measure `μ` and `f` is almost everywhere less than or equal to 0, the Lebesgue integral of `f` is equal to the Lebesgue integral over the interval from 0 to infinity of the measure of the set of elements `a` in `α` for which `f(a)` is greater than or equal to `t`. This is a version of the layer cake formula, Cavalieri's principle, or tail probability formula. There is another version of this theorem, `MeasureTheory.lintegral_eq_lintegral_meas_lt`, which considers sets of the form `{a | f(a) > t}` instead.
More concisely: For any measure space, nonnegative, almost everywhere measurable function `f` almost everywhere less than or equal to 0, the Lebesgue integral of `f` equals the integral from 0 to infinity of the measure of `{a : f(a) >= t}` with respect to `μ`.
|