MeasureTheory.lintegral_liminf_le'
theorem MeasureTheory.lintegral_liminf_le' :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
(∀ (n : ℕ), AEMeasurable (f n) μ) →
∫⁻ (a : α), Filter.liminf (fun n => f n a) Filter.atTop ∂μ ≤
Filter.liminf (fun n => ∫⁻ (a : α), f n a ∂μ) Filter.atTop
This is known as Fatou's lemma, stated in the context of almost-everywhere measurable functions. The lemma states that for any measurable space `α` and a measure `μ` defined on that space, if `f` is a sequence of functions that map each natural number `n` to an extended nonnegative real number for every element in `α` and each function in this sequence is almost-everywhere measurable with respect to `μ`, then the lower integral of the limit inferior of the sequence of functions `f` along the filter at infinity is less than or equal to the limit inferior along the filter at infinity of the lower integral of each function in the sequence. In mathematical notation, this can be expressed as:
\[ \int_{\alpha}\liminf_{n \to \infty}f_n(a)\,d\mu(a) \leq \liminf_{n \to \infty}\int_{\alpha}f_n(a)\,d\mu(a) \]
More concisely: The limit inferior of the integral of an almost-everywhere measurable sequence of extended nonnegative real-valued functions with respect to a measure is less than or equal to the integral of their limit inferior. In mathematical notation, this is written as:
\[ \int_{\alpha} \liminf_{n \to \infty} f_n(a) \,d\mu(a) \leq \liminf_{n \to \infty} \int_{\alpha} f_n(a) \,d\mu(a) \]
|
MeasureTheory.lintegral_le_of_forall_fin_meas_le
theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : MeasureTheory.SigmaFinite μ]
(C : ENNReal) {f : α → ENNReal},
AEMeasurable f μ →
(∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C) → ∫⁻ (x : α), f x ∂μ ≤ C
The theorem `MeasureTheory.lintegral_le_of_forall_fin_meas_le` states that for any measurable space `α` and a σ-finite measure `μ` on `α`, if a function `f` mapping from `α` to extended nonnegative real numbers is almost everywhere measurable and the Lebesgue integral of `f` over any measurable set `s` (where the measure of `s` is not infinity) is less than or equal to a constant `C`, then the integral of `f` over the entire space is also less than or equal to `C`.
In simpler terms, this theorem says that if the Lebesgue integral of a function is bounded by some constant on all finite-measure sets, then the integral over the entire space (under a σ-finite measure) is also bounded by that same constant.
More concisely: If `α` is a measurable space with a σ-finite measure `μ`, and a measurable function `f: α → ℝ∞:` satisfies `∫s.μ, f dμ ≤ C` for all measurable sets `s` with finite measure, then `∫α.μ, f dμ ≤ C`.
|
MeasureTheory.mul_meas_ge_le_lintegral₀
theorem MeasureTheory.mul_meas_ge_le_lintegral₀ :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
AEMeasurable f μ → ∀ (ε : ENNReal), ε * ↑↑μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
The Lean 4 statement describes **Markov's inequality**, also known as **Chebyshev's first inequality**. This theorem states that, for any measure space `α` with measure `μ` and any almost everywhere measurable function `f` from `α` to the extended nonnegative real numbers `ENNReal`, the product of any extended nonnegative real number `ε` and the measure of the set of elements `x` in `α` where `ε` is less than or equal to `f(x)` is less than or equal to the Lebesgue integral of `f` with respect to `μ`.
More concisely: For any measure space `(α, μ)`, and any almost everywhere measurable function `f : α → [0, +∞]`, we have ε · μ({x : α | f(x) ≤ ε}) ≤ ∫α f dμ.
|
MeasureTheory.exists_pos_set_lintegral_lt_of_measure_lt
theorem MeasureTheory.exists_pos_set_lintegral_lt_of_measure_lt :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
∫⁻ (x : α), f x ∂μ ≠ ⊤ →
∀ {ε : ENNReal}, ε ≠ 0 → ∃ δ > 0, ∀ (s : Set α), ↑↑μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
This theorem states that given a measure space `α` with a measurable space structure `m` and a measure `μ`, and a function `f` that maps this space to the extended nonnegative real numbers (`ENNReal`), if the integral of `f` over `α` is finite, then the integral of `f` over any subset `s` of `α` behaves in an absolutely continuous manner with respect to `μ`. More specifically, it establishes that for any positive `ε`, there exists a `δ` such that for all subsets `s` of `α` with measure `μ` less than `δ`, the integral of `f` over `s` is less than `ε`. This implies that as the measure of the subset `s` tends to zero, so does the integral of `f` over `s`.
More concisely: Given a measurable function `f` on a measure space `(α, μ)` with finite integral, for every `ε > 0`, there exists `δ > 0` such that for any measurable subset `s` of `α` with `μ(s) < δ`, the integral of `f` over `s` is less than `ε`.
|
MeasureTheory.lintegral_indicator
theorem MeasureTheory.lintegral_indicator :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {s : Set α},
MeasurableSet s → ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
The theorem `MeasureTheory.lintegral_indicator` states that for any measurable space `α`, any measure `μ` on that space, any function `f` from `α` to the extended nonnegative real numbers `ENNReal`, and any measurable set `s`, the Lebesgue integral over the whole space of the function `f` where it is multiplied by the indicator function of the set `s` (making it zero outside `s`) is equal to the Lebesgue integral of `f` over the set `s`. In other words, integrating a function over a whole space, but with the function's value being zero outside a particular set, is the same as integrating the function over that set itself. In LaTeX mathematics, it is represented as:
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {s : Set α}, MeasurableSet s → ∫⁻ (a : α), Set.indicator s f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
More concisely: For any measurable space, measure, function, and measurable set, the Lebesgue integral of the function's indicator multiplication over the whole space equals the integral over the set itself.
|
MeasureTheory.lintegral_def
theorem MeasureTheory.lintegral_def :
∀ {α : Type u_5} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
MeasureTheory.lintegral μ f = ⨆ g, ⨆ (_ : ↑g ≤ f), g.lintegral μ
The theorem `MeasureTheory.lintegral_def` states that for any measurable space `α` and a measure `μ` on that space, the lower Lebesgue integral of a function `f` mapping from `α` to the extended nonnegative real numbers is equal to the supremum of the integrals of all simple functions `g` that are less than or equal to `f`. This supremum is taken over all such simple functions `g` and their corresponding integral values calculated using the measure `μ`. In other words, in mathematical terms, if $\mu$ is a measure and $f: \alpha \rightarrow [0, \infty]$ is a function, then the lower Lebesgue integral of $f$ with respect to $\mu$ is given by $\sup \{\int g \, d\mu : g \text{ is a simple function and } g \leq f\}$.
More concisely: The lower Lebesgue integral of a measurable function with respect to a measure is equal to the supremum of the integrals of all simple functions less than or equal to it.
|
MeasureTheory.monotone_lintegral
theorem MeasureTheory.monotone_lintegral :
∀ {α : Type u_1} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), Monotone (MeasureTheory.lintegral μ) := by
sorry
The theorem `MeasureTheory.monotone_lintegral` states that for any measurable space `α` and any measure `μ` on this space, the function `MeasureTheory.lintegral μ` is monotone. In other words, given two functions `a` and `b` from `α` to the extended non-negative real numbers such that `a ≤ b`, it follows that the lower Lebesgue integral of `a` with respect to `μ` is less than or equal to the lower Lebesgue integral of `b` with respect to `μ`. This property is crucial in many parts of measure theory and integration theory.
More concisely: For any measurable space and measure, the integral operator is monotone, i.e., if `a ≤ b` are measurable functions, then `∫(a) dμ ≤ ∫(b) dμ`.
|
MeasureTheory.lintegral_const_mul
theorem MeasureTheory.lintegral_const_mul :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal},
Measurable f → ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
This theorem states that for any measurable space `α`, given a measure `μ` on `α`, a constant `r` of extended nonnegative real numbers (which includes the positive real numbers and positive infinity), and a measurable function `f` from `α` to the extended nonnegative real numbers, the integration of the function `f` multiplied by the constant `r` with respect to the measure `μ` is equal to the constant `r` times the integration of the function `f` with respect to the measure `μ`. In other words, it asserts the property of constant multiplication with respect to the Lebesgue integral, which is a fundamental property of integration in measure theory.
More concisely: For any measurable space, measure, constant, and measurable function, the integral of the constant times the function with respect to the measure equals the constant times the integral of the function with respect to the measure.
|
MeasureTheory.lintegral_iInf_ae
theorem MeasureTheory.lintegral_iInf_ae :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
(∀ (n : ℕ), Measurable (f n)) →
(∀ (n : ℕ), μ.ae.EventuallyLE (f n.succ) (f n)) →
∫⁻ (a : α), f 0 a ∂μ ≠ ⊤ → ∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
The Monotone Convergence Theorem for nonincreasing sequences of functions states that for any measurable space `α`, given a measure `μ` on `α` and a sequence of functions `f : ℕ → α → ENNReal` (from natural numbers to functions from `α` to extended nonnegative real numbers), if each function `f n` is measurable and for every natural number `n`, almost everywhere we have `f (n+1) ≤ f n` (i.e., the sequence of functions is nonincreasing almost everywhere), and if the integral over `α` with respect to `μ` of the zeroth function `f 0` is not infinity, then the integral of the infimum of the sequence of functions equals the infimum of the integrals of the functions in the sequence. In mathematical notation, we have
\[
∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
\]
provided the conditions mentioned above are satisfied.
More concisely: If `α` is a measurable space, `μ` a measure on `α`, and `f : ℕ → α → ENNReal` a sequence of measurable, nonincreasing functions almost everywhere, then `∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ` provided the integral of `f 0` is finite.
|
MeasureTheory.lintegral_add_measure
theorem MeasureTheory.lintegral_add_measure :
∀ {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal) (μ ν : MeasureTheory.Measure α),
∫⁻ (a : α), f a ∂(μ + ν) = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), f a ∂ν
This theorem, `MeasureTheory.lintegral_add_measure`, states that for any type `α`, a measurable space `m` of type `α`, a function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), and two measures `μ` and `ν` on `α`, the Lebesgue integral of `f` with respect to the measure (`μ + ν`) is equal to the sum of the Lebesgue integral of `f` with respect to `μ` and the Lebesgue integral of `f` with respect to `ν`. In mathematical terms, it says that the integral of `f` over `(μ + ν)` is the same as the integral of `f` over `μ` plus the integral of `f` over `ν`, symbolically expressed as $\int f d(μ + ν) = \int f dμ + \int f dν$.
More concisely: The Lebesgue integral of a measurable function with respect to the sum of two measures is equal to the sum of the integrals with respect to each measure.
|
MeasureTheory.lintegral_sum_measure
theorem MeasureTheory.lintegral_sum_measure :
∀ {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} (f : α → ENNReal) (μ : ι → MeasureTheory.Measure α),
∫⁻ (a : α), f a ∂MeasureTheory.Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
This theorem states that for any type `α` and `ι`, a measurable space `α`, a function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), and a measure `μ` indexed by `ι`, the Lebesgue integral of the function `f` with respect to the sum of the measures is equal to the sum of the Lebesgue integrals of the function `f` with respect to each measure individually. In mathematical terms, we can express this as $\int f d(\sum_i \mu_i) = \sum_i \int f d\mu_i$.
More concisely: The Lebesgue integral of a function with respect to the sum of measures is equal to the sum of integrals with respect to each measure.
|
MeasurableEmbedding.lintegral_map
theorem MeasurableEmbedding.lintegral_map :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSpace β]
{g : α → β},
MeasurableEmbedding g →
∀ (f : β → ENNReal), ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
The theorem `MeasurableEmbedding.lintegral_map` states that, given a measurable space `α`, a measure `μ` on `α`, a measurable space `β`, and a function `g : α → β` which is a measurable embedding, for any function `f : β → ENNReal` (where `ENNReal` is the extended nonnegative real numbers, typically denoted as `[0, ∞]`), the Lebesgue integral of `f` with respect to the pushforward measure `map g μ` is equal to the Lebesgue integral of the function `f ∘ g` with respect to the measure `μ`. This is a generalization of the theorem `lintegral_map`, except it does not require `f` to be measurable.
More concisely: Given a measurable space `α`, a measure `μ` on `α`, a measurable embedding `g : α → β`, and a function `f : β → [0, ∞]`, the Lebesgue integrals of `f` with respect to the measures `μ` and `map g μ` are equal.
|
MeasureTheory.lintegral_iSup_ae
theorem MeasureTheory.lintegral_iSup_ae :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
(∀ (n : ℕ), Measurable (f n)) →
(∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a) → ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
This theorem is a weaker version of the monotone convergence theorem in measure theory. It states that given any measurable space `α` and a measure `μ` on that space, if we have a sequence of functions `f : ℕ → α → ENNReal` (functions from natural numbers to functions from `α` to the extended nonnegative real numbers), where each function `f n` is measurable, and for all `n`, almost every `a` in `α` satisfies `f n a ≤ f n.succ a` (the sequence of functions is pointwise non-decreasing almost everywhere), then the integral of the supremum (over `n`) of the functions `f n` equals the supremum of the integrals of the functions. In LaTeX, this is saying:
For any measurable space `α`, measure `μ` on `α`, and sequence of measurable functions `f : ℕ → α → [0, ∞]` such that `f n ≤ f (n+1)` almost everywhere, we have
```latex
∫ α supₙ fₙ dμ = supₙ ∫ α fₙ dμ
```
It should be noted that this theorem only applies to extended nonnegative real-valued functions.
More concisely: Given a measurable space with a measure, if we have a sequence of measurable, pointwise non-decreasing functions from natural numbers to extended nonnegative real-valued functions, then the integral of the supremum of the functions equals the supremum of the integrals.
|
MeasureTheory.lintegral_add_right'
theorem MeasureTheory.lintegral_add_right' :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {g : α → ENNReal},
AEMeasurable g μ → ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
This theorem, `MeasureTheory.lintegral_add_right'`, states that for any type `α`, measurable space `m` of `α`, and measure `μ` on `α`, if we have two functions `f` and `g` mapping from `α` to the extended nonnegative real numbers (which include all nonnegative real numbers and positive infinity), and function `g` is almost everywhere measurable with respect to measure `μ`, then the integral over `μ` of the function `(a : α), f a + g a` (which is the function that adds the results of `f` and `g` at any given point) is equal to the sum of the integrals of `f` and `g` separately over `μ`. This is essentially a statement of linearity of integration in the context of measure theory.
More concisely: For measurable functions `f` and almost everywhere measurable `g` on a measurable space `(α, μ)` with values in the extended nonnegative real numbers, the integral of their sum `f + g` equals the sum of their integrals `∫(α, μ) (f + g) dμ = ∫(α, μ) fdμ + ∫(α, μ) gdμ`.
|
MeasureTheory.meas_ge_le_lintegral_div
theorem MeasureTheory.meas_ge_le_lintegral_div :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
AEMeasurable f μ → ∀ {ε : ENNReal}, ε ≠ 0 → ε ≠ ⊤ → ↑↑μ {x | ε ≤ f x} ≤ (∫⁻ (a : α), f a ∂μ) / ε
The theorem is a formalization of Markov's inequality, also known as Chebyshev's first inequality, in the context of measure theory. The inequality states that for any measure space `α`, given a measurable space `m`, a measure `μ` on `α`, and a function `f` from `α` to the extended nonnegative real numbers that is almost everywhere measurable with respect to `μ`, for any `ε` in the extended nonnegative real numbers that is not zero or infinity, the measure of the set of elements `x` in `α` for which `ε` is less than or equal to `f(x)` is less than or equal to the integral over `α` of `f` with respect to `μ` divided by `ε`. In simpler terms, this theorem states that the probability that a nonnegative function exceeds a certain value is at most the expected value of the function divided by that value.
More concisely: For any measure space, measure, and measurable function, the measure of the set where the function value is greater than a given value is less than or equal to the expected value of the function multiplied by the inverse of that value.
|
MeasureTheory.lintegral_congr_ae
theorem MeasureTheory.lintegral_congr_ae :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
μ.ae.EventuallyEq f g → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
This theorem, `MeasureTheory.lintegral_congr_ae`, states that for any type `α`, any measurable space `m` over `α`, any measure `μ` on that measurable space, and any two functions `f` and `g` from `α` to the extended nonnegative real numbers (ENNReal), if `f` and `g` are equal almost everywhere (i.e., they are equal except possibly on a set of measure zero), then the Lebesgue integrals of `f` and `g` with respect to the measure `μ` are also equal. In mathematical terms, it says that if $f = g$ almost everywhere (with respect to the measure $\mu$), then $\int f \, d\mu = \int g \, d\mu$. This theorem is a fundamental property of the Lebesgue integral, capturing the idea that the value of the integral is not affected by the function's values on a set of measure zero.
More concisely: If two measurable functions from a measurable space to the extended nonnegative real numbers are equal almost everywhere, then they have equal Lebesgue integrals with respect to a given measure.
|
NNReal.count_const_le_le_of_tsum_le
theorem NNReal.count_const_le_le_of_tsum_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] {a : α → NNReal},
Measurable a →
Summable a →
∀ {c : NNReal},
∑' (i : α), a i ≤ c → ∀ {ε : NNReal}, ε ≠ 0 → ↑↑MeasureTheory.Measure.count {i | ε ≤ a i} ≤ ↑c / ↑ε
This theorem, known as Markov's inequality for counting measure with hypothesis using `tsum` in nonnegative real numbers, states the following:
For any type `α`, with a measurable space structure and a measurable singleton class, and any function `a : α → NNReal` that is measurable and summable, if the sum of `a` over all `i : α` is less than or equal to a certain nonnegative real number `c`, then for any nonnegative real number `ε` that is not zero, the measure of the set of all `i` in `α` for which `a i` is greater than or equal to `ε` (computed using the counting measure) is less than or equal to `c` divided by `ε`.
In mathematical terms, if we have a summable function `a` from a measure space `α` to the nonnegative reals, and if the total sum of `a` is less than or equal to `c`, then the measure of the set where `a` exceeds `ε` is less than or equal to `c/ε`. This is a form of Markov's inequality, an important result in probability theory and statistics, in the context of measure theory.
More concisely: For any measurable function `a : α → ℝ+` from a measure space `α` to non-negative real numbers, if the sum of `a` is less than or equal to `c`, then the measure of the set where `a` exceeds `ε` is less than or equal to `c / ε`.
|
MeasureTheory.SimpleFunc.lintegral_eq_lintegral
theorem MeasureTheory.SimpleFunc.lintegral_eq_lintegral :
∀ {α : Type u_1} {m : MeasurableSpace α} (f : MeasureTheory.SimpleFunc α ENNReal) (μ : MeasureTheory.Measure α),
∫⁻ (a : α), ↑f a ∂μ = f.lintegral μ
The theorem `MeasureTheory.SimpleFunc.lintegral_eq_lintegral` states that for any measurable space `α`, any simple function `f` mapping from `α` to the extended nonnegative real numbers, and any measure `μ` on `α`, the Lebesgue integral of `f` with respect to `μ` is equal to the `lintegral` of `f` with respect to `μ`. In mathematical notation, for all `a` in `α`, the integral from negative infinity to infinity of `f(a)` with respect to `μ` (`∫⁻ (a : α), ↑f a ∂μ`) is equal to the `lintegral` of `f` with respect to `μ` (`MeasureTheory.SimpleFunc.lintegral f μ`). This theorem connects the concepts of Lebesgue integral and `lintegral` in the context of measure theory.
More concisely: For any measurable space, simple function, and measure, the Lebesgue integral and `lintegral` of the simple function with respect to the measure are equal.
|
MeasureTheory.set_lintegral_mono
theorem MeasureTheory.set_lintegral_mono :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal},
Measurable f → Measurable g → (∀ x ∈ s, f x ≤ g x) → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
The theorem `MeasureTheory.set_lintegral_mono` states that for any measurable space `α`, any measure `μ` on that space, any subset `s` of `α`, and any two functions `f` and `g` from `α` to the extended nonnegative real numbers (where extended nonnegative real numbers, denoted as [0, ∞], are used as the codomain of a measure), if both `f` and `g` are measurable and for every element `x` in `s`, `f(x)` is less than or equal to `g(x)`, then the set integral of `f` over `s` with respect to `μ` is less than or equal to the set integral of `g` over `s` with respect to `μ`. In mathematical terms, the theorem is stating that if `f` and `g` are measurable functions and `f(x) ≤ g(x)` for all `x` in a set `s`, then the Lebesgue integral of `f` over the set `s` is less than or equal to the Lebesgue integral of `g` over the same set `s`.
More concisely: If `f` and `g` are measurable functions on a measurable space `(α, Σ, μ)` with `f(x) ≤ g(x)` for all `x` in a set `s`, then ∫[s](f)dμ ≤ ∫[s](g)dμ. (Here, ∫[s](f)dμ denotes the set integral of `f` over `s` with respect to `μ`.)
|
MeasureTheory.lintegral_le_of_forall_fin_meas_le_of_measurable
theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le_of_measurable :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
[inst : MeasureTheory.SigmaFinite (μ.trim hm)] (C : ENNReal) {f : α → ENNReal},
Measurable f →
(∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C) → ∫⁻ (x : α), f x ∂μ ≤ C
The theorem, `MeasureTheory.lintegral_le_of_forall_fin_meas_le_of_measurable`, states that for any type `α`, given two measurable spaces `m` and `m0` over `α`, a measure `μ` on `α`, a sub-σ-algebra relationship `hm` between `m` and `m0`, a σ-finite measure with respect to `m`, a constant `C` of extended nonnegative real numbers, and a measurable function `f` from `α` to extended nonnegative real numbers. If for all measurable sets `s` with finite measure, i.e., the measure of `s` under `μ` is not infinity, the Lebesgue integral of `f` over `s` is less than or equal to `C`, then the Lebesgue integral of `f` over the entire measurable space is also less than or equal to `C`. The theorem is a version of the result specifically for measurable functions and assumes that the measure is σ-finite on the sub-σ-algebra.
More concisely: If `μ` is a σ-finite measure on measurable spaces `m` and `m0`, `hm` is a sub-σ-algebra relationship between `m` and `m0`, `f` is a measurable function from `α` to extended nonnegative real numbers, and for all measurable sets `s` with finite measure, the Lebesgue integral of `f` over `s` is less than or equal to a constant `C`, then the Lebesgue integral of `f` over the entire measurable space is also less than or equal to `C`.
|
MeasureTheory.lintegral_const
theorem MeasureTheory.lintegral_const :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal),
∫⁻ (x : α), c ∂μ = c * ↑↑μ Set.univ
The theorem `MeasureTheory.lintegral_const` states that for any measure space `α` with a measurable space structure `m` and a measure `μ`, and any nonnegative extended real number `c`, the Lebesgue integral of the constant function with value `c` with respect to the measure `μ` equals `c` times the measure of the universal set. In other words, it provides a formula for calculating the Lebesgue integral of a constant function over the entire space, which is simply the product of the constant and the measure of the whole space.
More concisely: For any measure space `(α, Σ, m, μ)` and constant function `c : ℝ↑`, the Lebesgue integral of `c` with respect to `μ` equals `c * μ(α)`.
|
MeasureTheory.lintegral_map
theorem MeasureTheory.lintegral_map :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β}
{f : β → ENNReal} {g : α → β},
Measurable f → Measurable g → ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
This theorem states that for any two measurable spaces `α` and `β`, with `α` having a measure `μ`, and for any two measurable functions `f` from `β` to extended nonnegative real numbers `[0, ∞]` and `g` from `α` to `β`, the Lebesgue integral (denoted by `∫⁻`) of `f` with respect to the pushforward of the measure `μ` by the function `g` is equal to the Lebesgue integral of the composition of `f` and `g` with respect to the measure `μ`. In mathematical terms, `∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ`. This is a theorem about the change of variables in Lebesgue integration.
More concisely: The Lebesgue integral of a measurable function `f` with respect to the pushforward measure of `μ` by `g` equals the Lebesgue integral of the composition `f ∘ g` with respect to the original measure `μ`.
|
MeasureTheory.lintegral_add_mul_meas_add_le_le_lintegral
theorem MeasureTheory.lintegral_add_mul_meas_add_le_le_lintegral :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
μ.ae.EventuallyLE f g →
AEMeasurable g μ → ∀ (ε : ENNReal), ∫⁻ (a : α), f a ∂μ + ε * ↑↑μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ
This is a version of Markov's inequality extended to two functions. The theorem states that for any measure space `α` with a measurable space `m` and a measure `μ`, and for two functions `f` and `g` from `α` to the extended nonnegative real numbers, if `f` is almost everywhere less than or equal to `g` and `g` is almost everywhere measurable, then for any `ε` in the extended nonnegative real numbers, the sum of the integral of `f` with respect to `μ` and `ε` times the measure of the set of `x` in `α` where `f x + ε` is less than or equal to `g x` is less than or equal to the integral of `g` with respect to `μ`. This theorem is interesting because the standard Markov's inequality assumes measurability only for `g` but not for `f`.
More concisely: For any measure space with measurable space and measure, and two functions from to the extended nonnegative real numbers with being almost everywhere less than or equal to almost everywhere measurable g, the integral of f with respect to μ and ε times the measure of {x | f(x) + ε < g(x)} is less than or equal to the integral of g with respect to μ.
|
MeasureTheory.lintegral_eq_zero_iff'
theorem MeasureTheory.lintegral_eq_zero_iff' :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
AEMeasurable f μ → (∫⁻ (a : α), f a ∂μ = 0 ↔ μ.ae.EventuallyEq f 0)
This theorem states that for any given measurable space `α`, measure `μ` on that space, and a function `f` from `α` to the extended nonnegative real numbers (usually denoted [0, ∞]), if the function `f` is almost everywhere measurable, then the Lebesgue integral (denoted ∫⁻ (a : α), f a ∂μ) of `f` with respect to measure `μ` is equal to 0 if and only if the function `f` is almost everywhere equal to 0 (with respect to the same measure `μ`). In other words, the Lebesgue integral of an almost everywhere measurable function is zero exactly when the function is zero almost everywhere.
More concisely: The Lebesgue integral of an almost everywhere measurable function equals 0 if and only if the function is almost everywhere equal to 0.
|
MeasureTheory.ae_lt_top
theorem MeasureTheory.ae_lt_top :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
Measurable f → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → ∀ᵐ (x : α) ∂μ, f x < ⊤
This theorem is in the context of measure theory. It states that for all types `α`, measurable spaces `m` on `α`, measures `μ` on `α`, and functions `f` from `α` to the extended nonnegative real numbers (ENNReal), if `f` is a measurable function and the integral (Lebesgue) of `f` with respect to measure `μ` is not infinity, then almost everywhere (`∀ᵐ` symbol denotes "almost everywhere") with respect to the measure `μ`, the value of `f` is less than infinity. In terms of measure theory, this is expressing that if the integral of a function over all space isn't infinite, the function value itself won't be infinite almost everywhere in the space.
More concisely: If `f` is a measurable function from a measurable space `(α, m)` to the extended nonnegative real numbers, with finite Lebesgue integral with respect to measure `μ`, then `μ`-almost everywhere, `f` is finite.
|
MeasureTheory.set_lintegral_congr_fun
theorem MeasureTheory.set_lintegral_congr_fun :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} {s : Set α},
MeasurableSet s → (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
The theorem `MeasureTheory.set_lintegral_congr_fun` states that for any measurable space `α` with a measure `μ`, and any two functions `f` and `g` from `α` to the extended nonnegative real numbers `ENNReal`, if we have a measurable set `s` in `α` such that almost everywhere in `s` (with respect to the measure `μ`), `f` and `g` are equal, then the integral over `s` of `f` with respect to `μ` is equal to the integral over `s` of `g` with respect to `μ`. In mathematical terms, this means that if two functions are equal almost everywhere in a measurable set, then their integrals over that set are also equal.
More concisely: If measurable functions `f` and `g` are equal almost everywhere on a measurable set `s` in a measurable space with measure `μ`, then their integrals over `s` with respect to `μ` are equal: `∫(s, μ, f) = ∫(s, μ, g)`.
|
MeasureTheory.lintegral_dirac'
theorem MeasureTheory.lintegral_dirac' :
∀ {α : Type u_1} [inst : MeasurableSpace α] (a : α) {f : α → ENNReal},
Measurable f → ∫⁻ (a : α), f a ∂MeasureTheory.Measure.dirac a = f a
This theorem states that for any type `α` that has a measurable space instance, any element `a` of type `α`, and any measurable function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), the Lebesgue integral of `f` with respect to the Dirac measure at `a` equals the function `f` evaluated at `a`. In other words, when integrating a measurable function over a Dirac measure, the integral is simply the value of the function at the point where the Dirac measure is centered.
More concisely: For any measurable function `f` from a measurable space `(α, Σ)` to the extended nonnegative real numbers, and any `α` element `a` with a measurable space instance, the Lebesgue integral of `f` with respect to the Dirac measure at `a` equals `f a`.
|
MeasureTheory.lintegral_iSup'
theorem MeasureTheory.lintegral_iSup' :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
(∀ (n : ℕ), AEMeasurable (f n) μ) →
(∀ᵐ (x : α) ∂μ, Monotone fun n => f n x) → ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
The Monotone Convergence Theorem (or Beppo-Levi Convergence), in the context of alomst everywhere measurable functions, states the following: For any measurable space `α`, and any measure `μ` on this space, if we have a sequence of functions from `α` to the extended nonnegative real numbers (`ENNReal`), where each function is almost everywhere measurable, and for almost every `x` in `α`, the function `n => f n x` is monotone, then the integral over `α` of the least upper bound (`⨆ n, f n a`) of each function in the sequence equals the least upper bound of the integrals of each function in the sequence. In other words, under these conditions, we can exchange the order of integration and taking supremum.
More concisely: If `{f_n : α → ENNReal}` is a sequence of almost everywhere measurable, monotone functions on the measurable space `(α, μ)`, then `∫ α ⊤ (⨆ n, f_n) dμ = ⨆ n, ∫ α f_n dμ`.
|
MeasureTheory.lintegral_mono_set
theorem MeasureTheory.lintegral_mono_set :
∀ {α : Type u_1} {x : MeasurableSpace α} ⦃μ : MeasureTheory.Measure α⦄ {s t : Set α} {f : α → ENNReal},
s ⊆ t → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in t, f x ∂μ
The theorem `MeasureTheory.lintegral_mono_set` states that for any type `α`, MeasurableSpace `x` of type `α`, a measure `μ` on `α`, two sets `s` and `t` of type `α`, and a function `f` from `α` to the extended nonnegative real numbers (usually denoted [0, ∞]), if set `s` is a subset of set `t`, then the Lebesgue integral of `f` over set `s` with respect to measure `μ` is less than or equal to the Lebesgue integral of `f` over set `t` with respect to measure `μ`. This theorem is a statement about the monotonicity of the Lebesgue integral with respect to the set of integration.
More concisely: For any measurable space (α, μ), measurable sets s ⊆ t, and measurable function f: α → [0, ∞], the Lebesgue integral of f over s with respect to μ is less than or equal to the Lebesgue integral of f over t with respect to μ.
|
MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone
theorem MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal},
(∀ (n : ℕ), AEMeasurable (f n) μ) →
(∀ᵐ (x : α) ∂μ, Monotone fun n => f n x) →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (F x))) →
Filter.Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))
The Monotone Convergence Theorem with limits states the following: Given a set of measurable functions `f : ℕ → α → ENNReal` and a function `F : α → ENNReal` on a measurable space `α` with a measure `μ`, if each function `f n` for all `n` in `ℕ` is almost everywhere measurable with respect to `μ`, and for almost all `x` in `α` the sequence `f n x` is monotone, and also for almost all `x` in `α` the sequence `f n x` converges to `F x`, then the limit of the sequence of integrals of `f n` as `n` goes to infinity is the integral of `F`.
This theorem is a key result in measure theory, providing a crucial technique for swapping the order of a limit and an integral in the case of nonnegative functions.
More concisely: If a sequence of measurable functions `f n : ℕ → α → ENNReal` on a measurable space `(α, μ)` is almost everywhere monotone and convergent to a measurable function `F : α → ENNReal`, then the integral of `F` is the limit of the integrals of `f n`.
|
MeasureTheory.lintegral_iSup_directed_of_measurable
theorem MeasureTheory.lintegral_iSup_directed_of_measurable :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable β]
{f : β → α → ENNReal},
(∀ (b : β), Measurable (f b)) →
Directed (fun x x_1 => x ≤ x_1) f → ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
The theorem `MeasureTheory.lintegral_iSup_directed_of_measurable` states that under certain conditions, the Lebesgue integral of a supremum over a directed family of functions is equal to the supremum of the Lebesgue integrals of the functions in the family. This is known as the monotone convergence theorem for supremums over directed families.
Here, the conditions are that the functions in the family are measurable, the family is directed under the order relation "less than or equal to", and the index set for the family is countable. More specifically, given a measurable space `α`, a measure `μ` on this space, a countable type `β`, and a family of functions `f : β → α → ENNReal` (functions from `β` to the extended nonnegative real numbers over `α`), if every function `f b` for `b` in `β` is measurable and the family of functions `f` is directed (i.e., for any `x` and `y` in `β`, there exists a `z` in `β` such that `f x ≤ f z` and `f y ≤ f z`), then the integral of the supremum of the functions in the family equals the supremum of the integrals of the functions.
More concisely: If `μ` is a measure on a measurable space `α`, `β` is a countable type, `f : β → α → ENNReal` is a family of measurable functions from `β` to the extended nonnegative real numbers over `α`, and the family `f` is directed, then `∫(sup(f b)) dμ = sup(∫(fb) dμ)`.
|
MeasureTheory.tendsto_measure_of_ae_tendsto_indicator
theorem MeasureTheory.tendsto_measure_of_ae_tendsto_indicator :
∀ {α : Type u_5} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_6} (L : Filter ι)
[inst_1 : L.IsCountablyGenerated] {As : ι → Set α} {μ : MeasureTheory.Measure α},
MeasurableSet A →
(∀ (i : ι), MeasurableSet (As i)) →
∀ {B : Set α},
MeasurableSet B →
↑↑μ B ≠ ⊤ →
(∀ᶠ (i : ι) in L, As i ⊆ B) →
(∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) →
Filter.Tendsto (fun i => ↑↑μ (As i)) L (nhds (↑↑μ A))
This theorem states that if we have a sequence (or more generally, a filter) of measurable sets `Aᵢ`, and the indicator functions of these sets converge almost everywhere to the indicator function of another measurable set `A`, then under certain conditions, the measures of the sets `Aᵢ` also converge to the measure of `A`. The conditions are that we have some set `B` of finite measure such that eventually, each `Aᵢ` is a subset of `B`, and that the convergence of the indicator functions happens almost everywhere with respect to a given measure `μ`. This result combines the ideas of measure theory and topology, and its proof involves techniques from both areas.
More concisely: If a sequence of measurable sets `Aᵢ` has indicator functions converging almost everywhere to the indicator function of a measurable set `A` on a measure space `(X, µ)` with respect to `µ` and there exists a set `B` of finite measure such that `B` contains `Aᵢ` for all large enough `i`, then `µ(Aᵢ)` converges to `µ(A)`.
|
MeasureTheory.lintegral_mono
theorem MeasureTheory.lintegral_mono :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} ⦃f g : α → ENNReal⦄,
f ≤ g → ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
The `MeasureTheory.lintegral_mono` theorem states that, for any type `α`, any measurable space `m` over `α`, any measure `μ` on that measurable space, and any two functions `f` and `g` from `α` to the extended non-negative real numbers (`ENNReal`), if `f` is less than or equal to `g` (i.e., `f` is pointwise less than or equal to `g`), then the Lebesgue integral (`∫⁻`) of `f` with respect to `μ` is less than or equal to the Lebesgue integral of `g` with respect to `μ`. This theorem formalizes the idea that, in measure theory, the integral of a function is monotonic with respect to pointwise order.
More concisely: If `α` is a type, `m` is a measurable space over `α`, `μ` is a measure on `m`, `f` and `g` are functions from `α` to the extended non-negative real numbers, and `f ≤ g` pointwise, then `∫⁻ f dμ ≤ ∫⁻ g dμ`.
|
MeasureTheory.lintegral_le_of_forall_fin_meas_le'
theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le' :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
[inst : MeasureTheory.SigmaFinite (μ.trim hm)] (C : ENNReal) {f : α → ENNReal},
AEMeasurable f μ →
(∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C) → ∫⁻ (x : α), f x ∂μ ≤ C
The theorem `MeasureTheory.lintegral_le_of_forall_fin_meas_le'` states that given a measure space `α` with two measurable spaces `m` and `m0` such that `m` is a sub-σ-algebra of `m0`, and a measure `μ` which is σ-finite on the sub-σ-algebra `m`, if for a function `f` from `α` to the extended nonnegative real numbers which is almost everywhere measurable with respect to `μ`, the Lebesgue integral of `f` over any set `s` with finite measure (i.e., `μ s` is not infinity) and which is a measurable set is less than or equal to some constant `C`, then the Lebesgue integral of `f` over the entire space `α` is also less than or equal to `C`. In other words, if the integral of a function is bounded by a constant on all sets with finite measure in a sub-σ-algebra, then the integral over the whole space is also bounded by that same constant.
More concisely: If `μ` is a σ-finite measure on the sub-σ-algebra `m` of a measure space `α`, `f` is an almost everywhere measurable function from `α` to the extended nonnegative real numbers, and for every measurable set `s` in `m` with finite measure `μ(s)`, the Lebesgue integral of `f` over `s` is bounded by a constant `C`, then the Lebesgue integral of `f` over the entire space `α` is also bounded by `C`.
|
MeasureTheory.lintegral_mul_const''
theorem MeasureTheory.lintegral_mul_const'' :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal},
AEMeasurable f μ → ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
The theorem `MeasureTheory.lintegral_mul_const''` states that for any measurable space `α`, any measure `μ` on that space, any extended nonnegative real number `r`, and any function `f` from `α` to the extended nonnegative real numbers that is almost everywhere measurable with respect to `μ`, the Lebesgue integral of the product of `f` and `r` with respect to `μ` is equal to the product of `r` and the Lebesgue integral of `f` with respect to `μ`. In short, it expresses the property that multiplication by a constant can be interchanged with the Lebesgue integral operation.
More concisely: For any measurable space α, measure μ, extended real number r, and almost everywhere measurable function f: ∫(r * f)(x) dμ(x) = r * ∫f(x) dμ(x).
|
MeasureTheory.lintegral_tsum
theorem MeasureTheory.lintegral_tsum :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable β]
{f : β → α → ENNReal},
(∀ (i : β), AEMeasurable (f i) μ) → ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ
This theorem, `MeasureTheory.lintegral_tsum`, states that for any measure space `α` with a measure `μ`, and for any countable type `β`, if we have a function `f` from `β` and `α` to the extended nonnegative real numbers (`ENNReal`) that is almost everywhere measurable for each `i` in `β`, then the integral over `α` of the sum of `f i a` over `i` in `β` (with respect to the measure `μ`) is equal to the sum over `i` in `β` of the integral over `α` of `f i a` (with respect to the measure `μ`).
In mathematical terms, if `f : β → α → ENNReal` is almost everywhere measurable for each `i` in `β`, then we have the equality:
```
∫⁻ a, (∑' i, f i a) dμ = ∑' i, ∫⁻ a, f i a dμ
```
This is an application of Fubini's theorem to the extended nonnegative real numbers, allowing us to interchange the order of summation and integration.
More concisely: For any measure space `(α, μ)` and countable family `{f_i : α → ENNReal}_{i ∈ β}` of almost everywhere measurable functions, we have:
∫⁻ a, (∑' i, f_i a) dμ = ∑' i, ∫⁻ a, f_i a dμ.
|
MeasureTheory.set_lintegral_univ
theorem MeasureTheory.set_lintegral_univ :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal),
∫⁻ (x : α) in Set.univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
This theorem, named `MeasureTheory.set_lintegral_univ`, states that for any type `α`, a measurable space `m` on `α`, a measure `μ` on `α`, and a function `f` from `α` to the extended nonnegative real numbers (usually denoted [0, ∞]), the set integral of `f` over the universal set (the set containing all elements of `α`) with respect to the measure `μ` is equal to the integral of `f` with respect to the measure `μ` without specifying a set. Here, ∫⁻ represents the Lebesgue integral or more specifically, the set integral with respect to a measure.
More concisely: For any measurable space `(α, m)`, measure `μ`, and measurable function `f` from `α` to [0, ∞], the set integral of `f` over the universal set with respect to `μ` equals the integral of `f` with respect to `μ`.
|
MeasureTheory.MeasurePreserving.set_lintegral_comp_emb
theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_emb :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mb : MeasurableSpace β}
{ν : MeasureTheory.Measure β} {g : α → β},
MeasureTheory.MeasurePreserving g μ ν →
MeasurableEmbedding g →
∀ (f : β → ENNReal) (s : Set α), ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν
This theorem states that for any types `α` and `β`, measurable spaces `m` and `mb`, measures `μ` and `ν` on these measurable spaces, and a function `g` from `α` to `β`, if `g` preserves the measure from `μ` to `ν` and `g` is a measurable embedding, then for any function `f` from `β` to the extended nonnegative real numbers and any set `s` of type `α`, the integral over `s` in `μ` of `f` composed with `g` is equal to the integral over the image of `s` under `g` in `ν` of `f`.
In simpler terms, if `g` is a measurable function that preserves measure, then the measure of a transformed set under a function `f` in the original measure is the same as the measure of the set in the transformed measure. This property is central to the theory of measure preserving transformations, which are key in areas such as ergodic theory and dynamical systems.
More concisely: If `g: α -> β` is a measurable embedding preserving measures `μ` and `ν` on measurable spaces `(α, Σα, μ)` and `(β, Σβ, ν)`, then for any `f: β -> [0, ∞]` and `s ∈ Σα`, we have `∫sμ = ∫g[s]ν. f`.
|
MeasureTheory.mul_meas_ge_le_lintegral
theorem MeasureTheory.mul_meas_ge_le_lintegral :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
Measurable f → ∀ (ε : ENNReal), ε * ↑↑μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
The theorem states Markov's inequality, which is also known as Chebyshev's first inequality in the context of measure theory. For any measurable space `α`, a measure `μ` on `α`, a measurable function `f` from `α` to the extended nonnegative real numbers, and any extended nonnegative real number `ε`, the measure of the set of elements in `α` where `f` exceeds `ε`, multiplied by `ε`, is less than or equal to the integral over `α` of `f` with respect to `μ`. In other words, it states that the quantity `ε * μ({x | ε ≤ f(x)})` is less than or equal to the Lebesgue integral of `f` over the measure space `α`.
More concisely: For any measurable function `f` and measure `μ` on a measurable space `α`, and for any extended nonnegative real number `ε`, the measure of the set of elements where `f` exceeds `ε` is less than or equal to `ε` times the integral of `f` with respect to `μ`.
|
MeasureTheory.lintegral_smul_measure
theorem MeasureTheory.lintegral_smul_measure :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) (f : α → ENNReal),
∫⁻ (a : α), f a ∂c • μ = c * ∫⁻ (a : α), f a ∂μ
This theorem, `MeasureTheory.lintegral_smul_measure`, states that for any type `α`, any measurable space `m` derived from `α`, any measure `μ` on that measurable space, and any function `f` from `α` to the extended non-negative real numbers, the Lebesgue integral of `f` with respect to the measure obtained by scaling `μ` by a constant `c` (denoted `c • μ`) is equal to `c` times the integral of `f` with respect to `μ`. In mathematical terms, it denotes that ∫⁻ f d(cμ) = c ∫⁻ f dμ, where ∫⁻ represents the Lebesgue integral.
More concisely: For any measurable function `f` from a measurable space `(α, m)` to the extended non-negative reals, and any constant `c > 0`, the Lebesgue integral of `f` with respect to the scaled measure `c * m` equals `c` times the integral of `f` with respect to the original measure `m`. In mathematical notation: ∫⁻ f d(c * m) = c * ∫⁻ f dm.
|
MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure
theorem MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure :
∀ {α : Type u_5} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_6} (L : Filter ι) {As : ι → Set α}
[inst_1 : L.IsCountablyGenerated] {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.IsFiniteMeasure μ],
MeasurableSet A →
(∀ (i : ι), MeasurableSet (As i)) →
(∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) → Filter.Tendsto (fun i => ↑↑μ (As i)) L (nhds (↑↑μ A))
The theorem `MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure` states that:
Given a finite measure `μ` over a measurable space `α`, a measurable set `A` in `α`, a filter `L` on an index set `ι`, and a function `As` from `ι` to measurable sets in `α`, if the filter `L` is countably generated and the indicator functions of the measurable sets `As(i)` converge pointwise almost everywhere to the indicator function of the set `A` with respect to the measure `μ`, then the measures `μ(As(i))` tend to the measure `μ(A)` in the sense that for every neighborhood of `μ(A)`, there is a neighborhood of `L` such that the measure of `As(i)` for every `i` in this neighborhood of `L` is contained in the neighborhood of `μ(A)`.
In simpler words, if the characteristic functions of a sequence of sets converge almost everywhere to the characteristic function of a set under a finite measure, then the sequence of measures of these sets also converges to the measure of the limit set.
More concisely: If `μ` is a finite measure on a measurable space, `A` is a measurable set, `L` is a countably generated filter on an index set, and `As(i)` is a sequence of measurable sets with indicator functions converging almost everywhere to `A`'s indicator function, then `μ(As(i))` converges to `μ(A)`.
|
MeasureTheory.lintegral_eq_iSup_eapprox_lintegral
theorem MeasureTheory.lintegral_eq_iSup_eapprox_lintegral :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
Measurable f → ∫⁻ (a : α), f a ∂μ = ⨆ n, (MeasureTheory.SimpleFunc.eapprox f n).lintegral μ
This theorem, `MeasureTheory.lintegral_eq_iSup_eapprox_lintegral`, states that for any measurable space `α`, a measure `μ` on `α`, and a measurable function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), the Lebesgue integral of `f` with respect to `μ` is equal to the supremum over all natural numbers `n` of the integral of the `n`-th approximation of `f` by simple functions. In other words, the Lebesgue integral of any measurable function can be approximated by the integral of a sequence of simple functions.
More concisely: For any measurable space `α`, measure `μ` on `α`, and measurable function `f` from `α` to the extended nonnegative real numbers, the Lebesgue integral of `f` with respect to `μ` equals the supremum of the integrals of `n`-th approximations of `f` by simple functions, where the approximations are taken over all natural numbers `n`.
|
MeasureTheory.lintegral_eq_nnreal
theorem MeasureTheory.lintegral_eq_nnreal :
∀ {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal) (μ : MeasureTheory.Measure α),
∫⁻ (a : α), f a ∂μ =
⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ
The theorem `MeasureTheory.lintegral_eq_nnreal` states that for any measurable space `α`, a function `f : α → ENNReal`, and a measure `μ : MeasureTheory.Measure α`, the Lebesgue integral `∫⁻ (a : α), f a ∂μ`, which is defined as the supremum of integrals of simple functions `φ : α →ₛ ℝ≥0∞` that are less than or equal to `f`, can indeed be computed by considering only simple functions `φ : α →ₛ ℝ≥0`. In other words, it's sufficient to take simple functions that map into nonnegative real numbers instead of extended nonnegative real numbers, and then map those values into the extended nonnegative real numbers using `ENNReal.ofNNReal`. This theorem underlines a crucial simplification in the computation of the Lebesgue integral.
More concisely: The theorem `MeasureTheory.lintegral_eq_nnreal` asserts that the Lebesgue integral of a measurable function `f : α → ENNReal` with respect to a measure `μ : MeasureTheory.Measure α` can be computed as the supremum of integrals of simple functions `φ : α →ₛ ℝ≥0` without the need to consider simple functions mapping into extended nonnegative real numbers.
|
MeasureTheory.lintegral_zero_measure
theorem MeasureTheory.lintegral_zero_measure :
∀ {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal), ∫⁻ (a : α), f a ∂0 = 0
The theorem `MeasureTheory.lintegral_zero_measure` states that for any type `α` and any measurable space `m` over `α`, the Lebesgue integral (denoted by `∫⁻`) of any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`, usually denoted as [0, ∞]) with respect to the zero measure (denoted by ∂0) is equal to zero. In essence, it is saying that if we measure a function over a space where the measure of every set is zero, then the total "amount" of the function, as measured by the Lebesgue integral, is zero.
More concisely: For any measurable space with zero measure and any measurable function to the extended nonnegative reals, the Lebesgue integral equals zero.
|
MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite
theorem MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ]
{ε : ENNReal}, ε ≠ 0 → ∃ g, (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ε
This theorem states that in a sigma-finite measure space, for any non-zero extended nonnegative real number (represented as `ENNReal` in Lean), there exists a function that is integrable, positive at every point in the measure space, and whose integral (calculated with respect to the given measure) is less than the given non-zero extended nonnegative real number. This function is also measurable, meaning that the preimage of any measurable set under this function is also a measurable set. Sigma-finite measure spaces are spaces where the total measure can be decomposed into a countable union of sets with finite measure.
More concisely: In a sigma-finite measure space, for every non-zero extended non-negative real number, there exists a measurable, positive function whose integral is strictly less than that number.
|
MeasureTheory.tendsto_lintegral_of_dominated_convergence'
theorem MeasureTheory.tendsto_lintegral_of_dominated_convergence' :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal}
(bound : α → ENNReal),
(∀ (n : ℕ), AEMeasurable (F n) μ) →
(∀ (n : ℕ), μ.ae.EventuallyLE (F n) bound) →
∫⁻ (a : α), bound a ∂μ ≠ ⊤ →
(∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))
This theorem is a version of the Dominated Convergence Theorem, a fundamental result in measure theory, tailored to nonnegative functions which are almost everywhere measurable. In essence, it states the following: Given a sequence of almost everywhere measurable functions `(F n)` from a measure space to the nonnegative extended real numbers, a function `f` from the same measure space to the nonnegative extended real numbers, and a bounding function `bound` such that each `F n` is almost everywhere less than or equal to `bound`, and that the integral of `bound` is finite. If for almost all points in the measure space, the sequence `(F n)` converges to `f` as `n` tends to infinity, then the sequence of integrals of `F n` also converges to the integral of `f` as `n` tends to infinity.
More concisely: If `(F n)` is a sequence of almost everywhere measurable, nonnegative functions on a measure space converging almost everywhere to a function `f`, and each `F n` is pointwise dominated by a bounded function `bound`, then the integral of `F n` converges to the integral of `f`.
|
MeasureTheory.lintegral_iInf_directed_of_measurable
theorem MeasureTheory.lintegral_iInf_directed_of_measurable :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : Countable β] {f : β → α → ENNReal}
{μ : MeasureTheory.Measure α},
μ ≠ 0 →
(∀ (b : β), Measurable (f b)) →
(∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤) →
Directed (fun x x_1 => x ≥ x_1) f → ∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
The theorem "MeasureTheory.lintegral_iInf_directed_of_measurable" states that for a directed family of functions `f : β → α → ENNReal` indexed by a countable set `β`, where each `f b` (for `b` in `β`) is a measurable function and its integral over a non-zero measure space `α` with respect to a measure `μ` is not infinite, the integral over `α` of the infimum of the family of functions is equal to the infimum of the integrals of the functions in the family.
In other words, this theorem is about the exchange of integral and infimum over a directed family of functions when the functions are measurable and the integral of each function is not infinite.
More concisely: For a countable, directed family of measurable functions `f : β → α → ℝ` with finite integrals with respect to a measure `μ` on the measurable space `α`, the integral of the infimum of the family equals the infimum of the integrals.
|
MeasureTheory.tendsto_lintegral_of_dominated_convergence
theorem MeasureTheory.tendsto_lintegral_of_dominated_convergence :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal}
(bound : α → ENNReal),
(∀ (n : ℕ), Measurable (F n)) →
(∀ (n : ℕ), μ.ae.EventuallyLE (F n) bound) →
∫⁻ (a : α), bound a ∂μ ≠ ⊤ →
(∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))
This is the Dominated Convergence Theorem for nonnegative functions. It states that given a measurable space `α` with a measure `μ`, a sequence of functions `F : ℕ → α → ENNReal` and a function `f : α → ENNReal` bounded by another function `bound : α → ENNReal`, if each function in the `F` sequence is measurable and is almost everywhere less than or equal to the bounding function `bound` (whose integral over the space is finite), and if for almost all `a` in `α`, `F n a` converges to `f a` as `n` tends to infinity, then the sequence of integrals of the functions in `F` also converges to the integral of `f` as `n` tends to infinity.
In mathematical terms, it asserts that if `∀n, F n ≤ bound` almost everywhere and `∫ bound dμ < ∞`, and `F n` converges to `f` almost everywhere as `n → ∞`, then `∫ F n dμ → ∫ f dμ` as `n → ∞`.
More concisely: If `{F : ℕ → α → ENNReal}` is a sequence of measurable functions on a measurable space `(α, μ)` with `F n ≤ bound` almost everywhere, `bound` integrable, and `F n` converging almost everywhere to `f`, then `∫ F n dμ` converges to `∫ f dμ`.
|
MeasureTheory.lintegral_zero
theorem MeasureTheory.lintegral_zero :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, ∫⁻ (x : α), 0 ∂μ = 0
This theorem states that for any type `α`, any measurable space `m` on `α`, and any measure `μ` on this measurable space, the Lebesgue integral (notated as `∫⁻`) of the constant zero function over the measure `μ` is zero. In other words, the integral of zero over any space, under any measure, is always zero.
More concisely: For any measurable space `(α, m)` and measure `μ` on `α`, the Lebesgue integral of the constant zero function over `μ` is equal to zero.
|
MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence
theorem MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5} {l : Filter ι}
[inst : l.IsCountablyGenerated] {F : ι → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal),
(∀ᶠ (n : ι) in l, Measurable (F n)) →
(∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) →
∫⁻ (a : α), bound a ∂μ ≠ ⊤ →
(∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) l (nhds (f a))) →
Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) l (nhds (∫⁻ (a : α), f a ∂μ))
The Dominated Convergence Theorem for filters with a countable basis asserts that, given a measurable space `α` with a measure `μ` and a filter `l` on a type `ι` which has a countably generated basis, if we have a sequence of functions `F : ι → α → ENNReal` and another function `f : α → ENNReal`, along with a bounding function `bound : α → ENNReal` such that:
1. For almost all `n` in `l`, `F n` is measurable,
2. For almost all `n` in `l`, `F n a` is less than or equal to `bound a` for almost every `a` in `α` with respect to the measure `μ`,
3. The integral of `bound` with respect to `μ` is not infinite,
4. For almost every `a` in `α` with respect to the measure `μ`, the sequence `F n a` converges to `f a` as `n` tends to `l`.
Then, the sequence of the integrals of `F n` with respect to `μ` converges to the integral of `f` with respect to `μ` as `n` tends to `l`. This theorem is a key result in measure theory and provides conditions under which the limit of the integral of a sequence of functions is the integral of the limit function.
More concisely: Given a measurable space with a countably generated filter, a sequence of measurable functions `F : ι → α → ENNReal`, a function `f : α → ENNReal`, and a bounding function `bound : α → ENNReal` satisfying conditions 1-4 in the theorem description, the integral of `F n` with respect to `μ` converges to the integral of `f` with respect to `μ` as `n` tends to the filter `l`.
|
MeasureTheory.tendsto_set_lintegral_zero
theorem MeasureTheory.tendsto_set_lintegral_zero :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5} {f : α → ENNReal},
∫⁻ (x : α), f x ∂μ ≠ ⊤ →
∀ {l : Filter ι} {s : ι → Set α},
Filter.Tendsto (↑↑μ ∘ s) l (nhds 0) → Filter.Tendsto (fun i => ∫⁻ (x : α) in s i, f x ∂μ) l (nhds 0)
The theorem `MeasureTheory.tendsto_set_lintegral_zero` states that for a given measurable space `α` and a measure `μ` on that space, if we have a function `f` from `α` to the extended nonnegative real numbers (represented as `ENNReal`), which has a finite integral, then the set-integral of `f` over a set `s` (`∫⁻ x in s, f x ∂μ`) is absolutely continuous in `s`. This means that as the measure of the set `s` tends to zero (denoted as `Filter.Tendsto (↑↑μ ∘ s) l (nhds 0)`), the set-integral of `f` over `s` also tends to zero (denoted as `Filter.Tendsto (fun i => ∫⁻ (x : α) in s i, f x ∂μ) l (nhds 0)`). In other words, if a set is getting smaller, then the integral of `f` over this set is also getting closer to zero.
More concisely: Given a measurable space `α` with measure `μ`, if `f` is a measurable function from `α` to the extended nonnegative real numbers with finite integral, then the set-integral of `f` over any set `s` with shrinking measure tends to zero.
|
MeasureTheory.lintegral_mono_ae
theorem MeasureTheory.lintegral_mono_ae :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
(∀ᵐ (a : α) ∂μ, f a ≤ g a) → ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
This theorem, named `MeasureTheory.lintegral_mono_ae`, states that for any measurable space `α` and any measure `μ` on this space, if `f` and `g` are two functions from `α` to the extended nonnegative real numbers `ENNReal`, and almost everywhere in `α` (with respect to the measure `μ`), `f(a)` is less than or equal to `g(a)`, then the Lebesgue integral (also known as the lower Lebesgue integral) of `f` with respect to the measure `μ` is less than or equal to the Lebesgue integral of `g` with respect to the same measure. In other words, if one function is almost everywhere less than or equal to another, then its integral is also less than or equal to the integral of the other function.
More concisely: If `α` is a measurable space with measure `μ`, `f` and `g` are measurable functions from `α` to the extended nonnegative real numbers, and `μ`-almost everywhere `f(a) ≤ g(a)`, then `∫f dμ ≤ ∫g dμ`.
|
MeasureTheory.lintegral_iSup_directed
theorem MeasureTheory.lintegral_iSup_directed :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable β]
{f : β → α → ENNReal},
(∀ (b : β), AEMeasurable (f b) μ) →
Directed (fun x x_1 => x ≤ x_1) f → ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
The theorem `MeasureTheory.lintegral_iSup_directed` states that, given a directed family of functions `f` from the countable type `β` to the function space from `α` to the extended nonnegative real numbers `ENNReal`, where every member of the family is almost everywhere measurable, and the direction is in terms of less than or equal to relation, the order of taking supremum (`⨆`) and the Lebesgue integral (`∫⁻`) can be interchanged. In other words, the Lebesgue integral of the supremum over the family of functions at each point in `α` is equal to the supremum of the Lebesgue integral of each function in the family.
More concisely: For a directed family of almost everywhere measurable functions from a countable type to the function space from another set to the extended nonnegative real numbers, the Lebesgue integral commutes with the supremum operator.
|
MeasureTheory.set_lintegral_const
theorem MeasureTheory.set_lintegral_const :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (c : ENNReal),
∫⁻ (x : α) in s, c ∂μ = c * ↑↑μ s
This theorem, `MeasureTheory.set_lintegral_const`, states that for any type `α`, any measurable space `m` of type `α`, any measure `μ` of the measurable space, any set `s` of type `α`, and any extended non-negative real number `c`, the Lebesgue integral (also known as set integral) of the constant function `c` over the set `s` with respect to the measure `μ` is equal to `c` times the measure of the set `s`. In other words, the integral of a constant over a set is just the constant times the measure of the set. This is a fundamental result in measure theory, reflecting that the integral effectively "sums up" the constant value over the extent of the set, as measured by `μ`.
More concisely: For any measurable space (α, m), measure μ, set s, and constant c, the Lebesgue integral of the constant function c over set s with respect to measure μ equals c times the measure of set s.
|
MeasureTheory.lintegral_iInf
theorem MeasureTheory.lintegral_iInf :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
(∀ (n : ℕ), Measurable (f n)) →
Antitone f → ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤ → ∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
The Monotone Convergence Theorem for nonincreasing sequences of functions states that, for any measurable space `α` with a given measure `μ`, and a sequence of measurable functions `f : ℕ → α → ENNReal` (from nonnegative integers to functions from `α` to the extended nonnegative real numbers), if every function `f n` in the sequence is measurable, the sequence is antitone (i.e., `a ≤ b` implies `f b ≤ f a`), and the Lebesgue integral of `f 0` with respect to `μ` is not infinity, then the Lebesgue integral with respect to `μ` of the infimum of `f n` for all `n` is equal to the infimum of the Lebesgue integrals of `f n` for all `n`. This is essentially saying that, under these conditions, we can swap the order of the operations of taking the infimum and taking the Lebesgue integral.
More concisely: If `α` is a measurable space with measure `μ`, `f : ℕ → α → ENNReal` is a sequence of measurable, antitone functions with finite Lebesgue integral of `f 0`, then the Lebesgue integral of the pointwise infimum of `f n` equals the infimum of the Lebesgue integrals of `f n`.
|
MeasureTheory.lintegral_trim
theorem MeasureTheory.lintegral_trim :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal},
Measurable f → ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
The theorem `MeasureTheory.lintegral_trim` states that for any type `α`, any two measurable spaces `m` and `m0` over `α`, any measure `μ` over `α`, and any measurable function `f` from `α` to the extended nonnegative real numbers, if `m` is a subspace of `m0` and the function `f` is measurable, then the Lebesgue integral (or `lintegral`) of `f` with respect to the trimmed measure `μ.trim hm` is equal to the `lintegral` of `f` with respect to the original measure `μ`. So, essentially, trimming the measure does not change the value of the `lintegral`.
More concisely: For measurable spaces `m` and `m0` over type `α`, measure `μ` over `α`, measurable function `f` from `α` to the extended nonnegative real numbers, if `m` is a subspace of `m0` and `f` is measurable, then `lintegral (f) (μ.trim hm) = lintegral (f) μ`.
|
MeasureTheory.lintegral_add_left
theorem MeasureTheory.lintegral_add_left :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
Measurable f → ∀ (g : α → ENNReal), ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
The theorem `MeasureTheory.lintegral_add_left` states that given two extended nonnegative real-valued functions `f` and `g` defined on a measurable space `α`, if the function `f` is measurable, then the Lebesgue integral of the sum of `f` and `g` is equal to the sum of the Lebesgue integrals of `f` and `g` individually under measure `μ`. This theorem assumes that `f` is integrable. There are also similar theorems that apply if `g` is measurable or integrable.
More concisely: If `f` is a measurable, extended nonnegative real-valued function integrable under measure `μ` on a measurable space `α`, then `∫(f + g) dμ = ∫(f) dμ + ∫(g) dμ`.
|
MeasureTheory.set_lintegral_one
theorem MeasureTheory.set_lintegral_one :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α), ∫⁻ (x : α) in s, 1 ∂μ = ↑↑μ s
This theorem, named `MeasureTheory.set_lintegral_one`, states that for any given type `α`, any measurable space `m` of type `α`, any measure `μ` of the `MeasureTheory.Measure` on `α`, and any set `s` of type `α`, the Lebesgue integral (notated as `∫⁻`) of the constant function `1` over the set `s` with respect to the measure `μ` equals the double coercion (notated as `↑↑`) of the measure `μ` applied to the set `s`. In other words, the integral of one over a set is just the measure of that set.
More concisely: For any measurable space `(α, m)`, measure `μ` on `α`, and set `s` in `α`, the Lebesgue integral of the constant function 1 over `s` equals the measure `μ(s)`.
|
ENNReal.count_const_le_le_of_tsum_le
theorem ENNReal.count_const_le_le_of_tsum_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] {a : α → ENNReal},
Measurable a →
∀ {c : ENNReal},
∑' (i : α), a i ≤ c → ∀ {ε : ENNReal}, ε ≠ 0 → ε ≠ ⊤ → ↑↑MeasureTheory.Measure.count {i | ε ≤ a i} ≤ c / ε
This theorem, known as Markov's inequality for counting measure with hypothesis using `tsum` in `[0, ∞]`, states that for any measurable space `α` with a measurable singleton class and a function `a: α → [0, ∞]` that is measurable, for any extended nonnegative real number `c`, if the sum over all `i` in `α` of `a(i)` is less than or equal to `c`, then for any other extended nonnegative real number `ε` that is not zero or infinity, the counting measure of the set of `i` for which `ε` is less than or equal to `a(i)` is less than or equal to `c` divided by `ε`.
In simpler terms, it provides a bound on the probability that a random variable exceeds a certain value in terms of the expected value of the random variable, in the context of counting measures and extended nonnegative real numbers.
More concisely: For any measurable space with a measurable singleton class, if the sum of values from a measurable function to [0, ∞] is less than or equal to a constant, then the counting measure of elements with value greater than or equal to a fraction of that constant is less than or equal to the sum divided by the fraction.
|
MeasureTheory.lintegral_const_mul'
theorem MeasureTheory.lintegral_const_mul' :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal),
r ≠ ⊤ → ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
This theorem, `MeasureTheory.lintegral_const_mul'`, states that for any type `α`, given a measurable space `m` of type `α`, a measure `μ` on this space, a constant `r` in the set of extended nonnegative real numbers (which is denoted by `[0, ∞]` and does not include positive infinity), and a function `f` mapping from `α` to the extended nonnegative real numbers, if `r` is not positive infinity, then the Lebesgue integral of the product of `r` and `f a` with respect to measure `μ` (denoted as `∫⁻ (a : α), r * f a ∂μ`) is equal to the product of `r` and the Lebesgue integral of `f a` with respect to measure `μ` (denoted as `r * ∫⁻ (a : α), f a ∂μ`). In other words, the constant can be factored out of the Lebesgue integral when it is not positive infinity.
More concisely: For any measurable space `(α, m)`, measure `μ`, constant `r ∈ [0, ∞)`, and measurable function `f` from `α` to `[0, ∞)`, if `r < ∞`, then `∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ`.
|
MeasureTheory.lintegral_one
theorem MeasureTheory.lintegral_one :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, ∫⁻ (x : α), 1 ∂μ = ↑↑μ Set.univ
This theorem states that for any type `α`, any measurable space `m` of type `α`, and any measure `μ` from the Measure Theory, the Lebesgue integral (denoted by ∫⁻) of the constant function 1 with respect to the measure `μ` is equal to the measure of the universal set (i.e., the set of all elements) of type `α`. In mathematical terms, it denotes that the integral over the entire space of the constant function 1 is just the total measure of the space.
More concisely: For any measurable space `(α, m)` and measure `μ` from Measure Theory, ∫⁻(1 dμ) = m α.
|
MeasureTheory.lintegral_mono_fn
theorem MeasureTheory.lintegral_mono_fn :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} ⦃f g : α → ENNReal⦄,
(∀ (x : α), f x ≤ g x) → MeasureTheory.lintegral μ f ≤ MeasureTheory.lintegral μ g
This theorem, `MeasureTheory.lintegral_mono_fn`, asserts that for any type `α`, any measurable space `m` of type `α`, and any measure `μ` of that measurable space, if we have two functions `f` and `g` that map from `α` to the extended nonnegative real numbers (denoted `[0, ∞]`), then if `f` is less than or equal to `g` at every point in `α`, the lower Lebesgue integral of `f` with respect to `μ` is less than or equal to the lower Lebesgue integral of `g` with respect to `μ`. This is a form of monotonicity property for the lower Lebesgue integral. In mathematical terms, if `∀x∈α, f(x) ≤ g(x)`, then `∫ f dμ ≤ ∫ g dμ`.
More concisely: If `α` is a type, `m` is a measurable space on `α`, `μ` is a measure on `m`, and `f` and `g` are measurable functions from `α` to `[0, ∞]` with `f(x) ≤ g(x)` for all `x ∈ α`, then `∫ f dμ ≤ ∫ g dμ`.
|
MeasureTheory.lintegral_eq_zero_iff
theorem MeasureTheory.lintegral_eq_zero_iff :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
Measurable f → (∫⁻ (a : α), f a ∂μ = 0 ↔ μ.ae.EventuallyEq f 0)
The theorem `MeasureTheory.lintegral_eq_zero_iff` states that for all measurable spaces `α` with `m` as its measure and `μ` as its measure, and for any function `f` from `α` to the extended nonnegative real numbers, if `f` is measurable, then the integral of `f` with respect to measure `μ` is equal to zero if and only if the function `f` is almost everywhere equal to zero (that is, equal to zero except on a set of measure zero).
More concisely: A measurable function `f` from a measurable space `(α, m)` to the extended nonnegative real numbers equals the integral of `f` with respect to measure `μ` if and only if it is almost everywhere equal to zero.
|
MeasureTheory.lintegral_iSup
theorem MeasureTheory.lintegral_iSup :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
(∀ (n : ℕ), Measurable (f n)) → Monotone f → ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
The Monotone Convergence Theorem, also known as Beppo-Levi Convergence, states that for any measurable space and measure, if we consider a sequence of measurable functions from the natural numbers to the extended nonnegative real numbers, then if every function in this sequence is measurable and the sequence is monotone, the integral over the supremum of the sequence of functions is equal to the supremum of the sequence of integrals of the functions. In mathematical notation, we could express this as: $$\int \bigvee_n f_n \, d\mu = \bigvee_n \int f_n \, d\mu$$ where the integral symbol ∫ denotes integration with respect to a measure µ, ⨆ denotes the supremum (least upper bound), and f_n represents the functions in the sequence.
More concisely: For any measurable space and measure, if we have a sequence of measurable functions from the natural numbers to the extended nonnegative real numbers that are monotone increasing, then the integral of their supremum is equal to the supremum of their integrals: $\int \bigvee\_n f\_n \, d\mu = \bigvee\_n \int f\_n \, d\mu$.
|
MeasureTheory.lintegral_add_right
theorem MeasureTheory.lintegral_add_right :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {g : α → ENNReal},
Measurable g → ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
The theorem `MeasureTheory.lintegral_add_right` states that for any two functions `f` and `g` mapping from a type `α` to the extended nonnegative real numbers (denoted `[0, ∞]`), if one of them (`g` in this case) is measurable, then the Lebesgue integral of the sum of `f` and `g` is equal to the sum of their individual Lebesgue integrals. This is done under the conditions that we have a measurable space `m` of type `α` and a measure `μ` on that space. This theorem assumes that function `g` is integrable. There are also other versions of this theorem, like `MeasureTheory.lintegral_add_left` and its variations, where different assumptions may apply.
More concisely: If `f` and `g` are functions from a measurable space `(α, m)` to `[0, ∞]`, `g` is measurable and integrable, then `∫(f + g) dμ = ∫(f) dμ + ∫(g) dμ`.
|
MeasureTheory.lintegral_dirac
theorem MeasureTheory.lintegral_dirac :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] (a : α) (f : α → ENNReal),
∫⁻ (a : α), f a ∂MeasureTheory.Measure.dirac a = f a
This theorem states that for any measurable space `α` with singleton measurability, and any function `f` from `α` to the extended nonnegative real numbers, the Lebesgue integral (denoted by `∫⁻ (a : α), f a ∂MeasureTheory.Measure.dirac a`) over the Dirac measure at a point `a` is equal to the value of `f` at `a`. In other words, when we compute the Lebesgue integral with respect to the Dirac measure at a point, we simply "pick out" the function's value at that point.
More concisely: For any measurable space `α` with singleton measurability and any measurable function `f` from `α` to the extended nonnegative real numbers, the Lebesgue integral of `f` with respect to the Dirac measure at a point `a` equals `f a`.
|
MeasureTheory.lintegral_add_left'
theorem MeasureTheory.lintegral_add_left' :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
AEMeasurable f μ → ∀ (g : α → ENNReal), ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
The theorem `MeasureTheory.lintegral_add_left'` states that for any measure space `α` with a measure `μ` and two functions `f` and `g` from `α` to the extended nonnegative real numbers (`ENNReal`), if `f` is almost everywhere measurable with respect to `μ`, then the integral of the function `(a : α), f a + g a` with respect to `μ` is equal to the sum of the integrals of the functions `(a : α), f a` and `(a : α), g a` with respect to `μ`. In other words, we can split the integral of a sum of two functions into the sum of their separate integrals, when one of the functions is almost everywhere measurable.
More concisely: If `μ` is a measure on `α` and `f, g : α → ENNReal` are almost everywhere equal almost everywhere measurable functions, then `∫(a : α, f a + g a) dμ = ∫(a : α, f a) dμ + ∫(a : α, g a) dμ`.
|
MeasureTheory.lintegral_map_equiv
theorem MeasureTheory.lintegral_map_equiv :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSpace β]
(f : β → ENNReal) (g : α ≃ᵐ β), ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map (⇑g) μ = ∫⁻ (a : α), f (g a) ∂μ
This theorem states that the Lebesgue integral, or `lintegral`, transforms appropriately under a measurable equivalence `g : α ≃ᵐ β`. This is to say that, given a MeasurableSpace `α` with a measure `μ`, a MeasurableSpace `β`, a function `f : β → ENNReal` (extended nonnegative real numbers), and a measurable equivalence `g : α ≃ᵐ β`, the Lebesgue integral of `f` with respect to the pushforward measure of `g` on `μ` is equal to the Lebesgue integral of `f` composed with `g` with respect to `μ`. This generalizes the transformation property of the Lebesgue integral to the case where the function being integrated is measurable with respect to the image measure under a measurable equivalence.
More concisely: Given measurable spaces `α` and `β`, measures `μ` on `α` and a pushforward measure `ν` on `β`, a measurable equivalence `g : α ≃ᵐ β`, and a measurable function `f : β → ℝ`, the Lebesgue integrals of `f` with respect to `μ` and `ν` are equal: `∫(f ∘ g) dμ = ∫f dν`.
|
MeasureTheory.lintegral_map'
theorem MeasureTheory.lintegral_map' :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β}
{f : β → ENNReal} {g : α → β},
AEMeasurable f (MeasureTheory.Measure.map g μ) →
AEMeasurable g μ → ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
The theorem `MeasureTheory.lintegral_map'` states that for all types `α` and `β`, with `m` being the measurable space over `α` and `μ` being a measure on `α`, and `mβ` being the measurable space over `β`. If `f` is a function from `β` to the extended nonnegative real numbers (`ENNReal`), and `g` is a function from `α` to `β`, then if `f` is almost everywhere measurable with respect to the measure obtained by pushing forward `μ` by `g` (denoted `MeasureTheory.Measure.map g μ`), and `g` is almost everywhere measurable with respect to `μ`, the Lebesgue integral of `f` with respect to the measure `MeasureTheory.Measure.map g μ` is equal to the Lebesgue integral of `f ∘ g` with respect to the measure `μ`.
In symbolic terms, we have:
∫⁻ (a : β), f a ∂(MeasureTheory.Measure.map g μ) = ∫⁻ (a : α), f (g a) ∂μ
This essentially means that integrating the function `f` after applying the measure transformation `g` is the same as integrating the composed function `f ∘ g` under the original measure `μ`.
More concisely: The Lebesgue integral of a almost everywhere measurable function `f` with respect to the pushforward measure obtained by applying a measurable function `g` is equal to the Lebesgue integral of `f` composed with `g` under the original measure.
|
MeasureTheory.le_lintegral_add
theorem MeasureTheory.le_lintegral_add :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : α → ENNReal),
∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a + g a ∂μ
The theorem `MeasureTheory.le_lintegral_add` states that for any measure space `α` with a measurable space `m` and a measure `μ`, and for any two functions `f` and `g` from `α` to the extended nonnegative real numbers (usually denoted [0, ∞]), the sum of the lower Lebesgue integrals of `f` and `g` is less than or equal to the lower Lebesgue integral of the sum of `f` and `g`. However, to establish the reverse inequality, one of these functions, `f` or `g`, needs to be almost everywhere measurable.
More concisely: For measurable functions `f` and `g` from a measure space `(α, σ, μ)` to the extended nonnegative real numbers, the lower Lebesgue integral of `f + g` is less than or equal to the sum of the lower Lebesgue integrals of `f` and `g`, but the reverse inequality holds if one of `f` or `g` is almost everywhere measurable.
|
MeasureTheory.exists_measurable_le_lintegral_eq
theorem MeasureTheory.exists_measurable_le_lintegral_eq :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
The theorem `MeasureTheory.exists_measurable_le_lintegral_eq` states that for any function `f` that maps elements of type `α` to the extended nonnegative real numbers (`ENNReal`), there exists a measurable function `g` such that `g` is less than or equal to `f` (pointwise) and the integral of `f` with respect to a measure `μ` is equal to the integral of `g` with respect to the same measure. This theorem is relevant in measure theory, an area of mathematics related to integrating functions over spaces, and it basically tells us that we can always find a measurable function that "fits under" our given function and has the same integral.
More concisely: For any extended non-negative real-valued function `f` on a measurable space, there exists a measurable function `g` such that `g ≤ f` pointwise and the integrals of `f` and `g` with respect to a given measure are equal.
|
MeasureTheory.lintegral_liminf_le
theorem MeasureTheory.lintegral_liminf_le :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
(∀ (n : ℕ), Measurable (f n)) →
∫⁻ (a : α), Filter.liminf (fun n => f n a) Filter.atTop ∂μ ≤
Filter.liminf (fun n => ∫⁻ (a : α), f n a ∂μ) Filter.atTop
This theorem is known as Fatou's Lemma. It states that for any measurable space `α` with measure `μ`, and any sequence of functions `f : ℕ → α → ENNReal` (mapping natural numbers to functions from `α` to the extended nonnegative real numbers), if each function `f n` is measurable, then the lower limit (or `liminf`) of the integral over `α` of the `liminf` of the sequence at each point, with respect to the measure `μ`, is less than or equal to the `liminf` of the sequence of integrals of each function in the sequence, as the index goes to infinity. This is fundamental result in measure theory that provides a lower bound for the integral of a limit of a sequence of functions.
More concisely: For any measurable space with measure, and any sequence of measurable functions from to the extended nonnegative real numbers, the liminf of the integral of the liminf of each function is less than or equal to the liminf of the integrals of the sequence.
|
MeasureTheory.lintegral_mono'
theorem MeasureTheory.lintegral_mono' :
∀ {α : Type u_1} {m : MeasurableSpace α} ⦃μ ν : MeasureTheory.Measure α⦄,
μ ≤ ν → ∀ ⦃f g : α → ENNReal⦄, f ≤ g → ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν
The theorem `MeasureTheory.lintegral_mono'` states that for any measurable space `α` and two measures `μ` and `ν` on that space, if `μ` is less than or equal to `ν` and `f` and `g` are two functions from `α` to the extended nonnegative real numbers (`ENNReal`), such that `f` is less than or equal to `g`, then the integral from `f` with respect to `μ` is less than or equal to the integral from `g` with respect to `ν`. In mathematical notation, this is written as: if `μ ≤ ν` and `f ≤ g`, then `∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν`. This theorem is a fundamental property of measures and integrals in measure theory.
More concisely: If `μ` is a measure less than or equal to `ν` on the measurable space `α`, and `f` is a measurable function with `f ≤ g` pointwise, then the integral of `f` with respect to `μ` is less than or equal to the integral of `g` with respect to `ν`.
|