MeasureTheory.measure_le_lintegral_pos
theorem MeasureTheory.measure_le_lintegral_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
[inst : MeasureTheory.IsProbabilityMeasure μ], AEMeasurable f μ → 0 < ↑↑μ {x | f x ≤ ∫⁻ (a : α), f a ∂μ}
The theorem, titled **First Moment Method**, states that for any measurable function mapped from a type `α` to the extended nonnegative real numbers, given a probability measure `μ`, if the function is almost everywhere measurable with respect to `μ`, then the measure of the set of elements from type `α` where the function is less than or equal to its integral (i.e., expected value) over `μ` is positive. In mathematical terms, for a function `f` and a measure `μ`, `μ({x | f(x) ≤ ∫ f dμ}) > 0`. This theorem is a foundation for the probabalistic method in combinatorics and computer science, and it essentially says that if the average (expected value) of a nonnegative function is positive, then there must be some point where the function is positive.
More concisely: For any measurable function `f` from type `α` to the extended nonnegative real numbers and probability measure `μ` on `α`, if `f` is almost everywhere measurable with respect to `μ` and the integral of `f` over `μ` is positive, then the measure of the set of elements in `α` where `f` is less than or equal to its integral is positive.
|
MeasureTheory.average_eq_integral
theorem MeasureTheory.average_eq_integral :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
(μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.IsProbabilityMeasure μ] (f : α → E),
⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ
The theorem `MeasureTheory.average_eq_integral` states that for any type `α`, any normed additive commutative group `E`, any measurable space `m0` on `α`, any normed space of real numbers `ℝ` on `E`, any measure `μ` on `α` that is a probability measure, and any function `f` from `α` to `E`, the Bochner (or Lebesgue) integral of `f` with respect to `μ` is equal to the expected value of `f` under the probability measure `μ`.
More concisely: For any measurable space `(α, Σ, μ)` where `μ` is a probability measure, the Bochner integral of a `Σ → ℝ` measurable function `f` equals the expected value of `f` under `μ`.
|
MeasureTheory.measure_le_integral_pos
theorem MeasureTheory.measure_le_integral_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
[inst : MeasureTheory.IsProbabilityMeasure μ],
MeasureTheory.Integrable f μ → 0 < ↑↑μ {x | f x ≤ ∫ (a : α), f a ∂μ}
This theorem is known as the "First Moment Method". It states that for any measurable space `α` with an associated probability measure `μ` and any integrable function `f` from `α` to the real numbers, the measure of the set of points where `f` is less than or equal to its own integral is positive. In other words, there exists a substantial set (in terms of probability measure) where the function's value does not exceed its average.
More concisely: For any measurable space with a probability measure and an integrable function, the set where the function's value is less than or equal to its integral has positive measure.
|
MeasureTheory.exists_le_setAverage
theorem MeasureTheory.exists_le_setAverage :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ},
↑↑μ s ≠ 0 → ↑↑μ s ≠ ⊤ → MeasureTheory.IntegrableOn f s μ → ∃ x ∈ s, f x ≤ ⨍ (a : α) in s, f a ∂μ
The theorem "First moment method" states that, for any measurable space `α`, any measure `μ` on that space, any set `s` of `α`, and any real-valued function `f` defined on `α`, provided that the measure of `s` is neither zero nor infinite and the function `f` is integrable over the set `s` with respect to the measure `μ`, there exists an element `x` in the set `s` such that the value of the function `f` at `x` is less than or equal to the average (mean) value of the function `f` over the set `s`, with respect to the measure `μ`. In mathematical notation, this is saying that if $\mu(s) \neq 0$ and $\mu(s) \neq \infty$, then $\exists x \in s: f(x) \leq \int_{a \in s} f(a) \, d\mu$.
More concisely: Given a measurable space `α`, a measure `μ`, a set `s` with finite positive measure, and an integrable real-valued function `f` on `s`, there exists an element `x` in `s` such that `f(x)` is less than or equal to the mean value of `f` over `s` with respect to `μ`.
|
MeasureTheory.exists_le_integral
theorem MeasureTheory.exists_le_integral :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
[inst : MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.Integrable f μ → ∃ x, f x ≤ ∫ (a : α), f a ∂μ
This theorem is referred to as the "First moment method". It states that for any measurable space `α`, measure `μ` over `α`, and integrable function `f` from `α` to real numbers, if the measure `μ` is a probability measure, then there exists a point `x` in `α` such that the value of the function `f` at `x` is less than or equal to the integral of `f` with respect to the measure `μ`. In mathematical terms, the theorem states: $\exists x, f(x) \leq \int f(a) d\mu$ where `μ` is a probability measure.
More concisely: If `μ` is a probability measure on the measurable space `(α, Σ)` and `f` is an integrable function from `α` to real numbers, then there exists an `x` in `α` such that `f(x) ≤ ∫f(a) dμ`.
|
MeasureTheory.measure_le_average_pos
theorem MeasureTheory.measure_le_average_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
[inst : MeasureTheory.IsFiniteMeasure μ],
μ ≠ 0 → MeasureTheory.Integrable f μ → 0 < ↑↑μ {x | f x ≤ ⨍ (a : α), f a ∂μ}
This is the First Moment Method theorem in measure theory. It states that for any measurable space `α` with a measure `μ` and an integrable function `f : α → ℝ`, assuming `μ` is a finite measure and not equal to zero, the measure of the set of elements `x` such that `f(x)` is less than or equal to the mean of `f` with respect to measure `μ`, is positive. This essentially means that an integrable function is less than its mean on a set of positive measure.
More concisely: For any measurable space with a finite, non-zero measure and an integrable function, the set of elements where the function value is less than or equal to the function's mean has positive measure.
|
MeasureTheory.exists_not_mem_null_average_le
theorem MeasureTheory.exists_not_mem_null_average_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ℝ}
[inst : MeasureTheory.IsFiniteMeasure μ],
μ ≠ 0 → MeasureTheory.Integrable f μ → ↑↑μ N = 0 → ∃ x ∉ N, ⨍ (a : α), f a ∂μ ≤ f x
The theorem, referred to as the "First moment method", states that for any measurable space `α`, measure `μ`, set `N` in `α`, and real-valued function `f` defined on `α`, if the measure `μ` is non-zero and finite, and the function `f` is integrable with respect to `μ`, and the measure of the set `N` is zero, then there exists an element `x` not in `N` such that the mean value of `f` (expressed as the integral of `f(a)` over `α` with respect to the measure `μ`) is less than or equal to `f(x)`. In other words, the maximum of an integrable function is greater than its mean, excluding a set with measure zero.
More concisely: For any measurable space `(α, Σ, μ)`, measurable set `N ∈ Σ` with zero measure, integrable function `f: α → ℝ`, and non-zero, finite measure `μ`, there exists an element `x ∈ α \ N` such that `∫(f(a) dμ) ≤ f(x)`.
|
MeasureTheory.average_zero_measure
theorem MeasureTheory.average_zero_measure :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
(f : α → E), ⨍ (x : α), f x ∂0 = 0
This theorem states that for any function `f` mapping from a measurable space `α` to a normed add commutative group `E` that's a normed space over the real numbers ℝ, the integral (denoted by `⨍`) of `f` with respect to the zero measure (denoted by `∂0`) is always zero. In other words, if you integrate a function over a space with zero measure, the result is zero. This is consistent with the intuitive sense that areas or volumes of "empty" sets are zero.
More concisely: For any measurable function `f` from a measurable space `α` to a normed add commutative group `E` over ℝ, the integral `⨍f d∂0` is equal to the zero element of `E`.
|
MeasureTheory.exists_not_mem_null_le_lintegral
theorem MeasureTheory.exists_not_mem_null_le_lintegral :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ENNReal}
[inst : MeasureTheory.IsProbabilityMeasure μ], AEMeasurable f μ → ↑↑μ N = 0 → ∃ x ∉ N, f x ≤ ∫⁻ (a : α), f a ∂μ
The theorem, often referred to as the "First Moment Method", states that for any given set `α`, a measurable space `m0`, a measure `μ`, a set `N` and a function `f` that maps `α` to the extended non-negative real numbers, and assuming that `μ` is a probability measure and `f` is almost everywhere measurable, if the measure of set `N` is zero, then there exists an element `x` that is not in `N` such that the value of the function `f` at `x` is less than or equal to the Lebesgue integral of `f` over the set `α`. In more mathematical terms, this theorem is saying that the minimum of a measurable function is smaller than or equal to its integral, excluding a null set.
More concisely: If `μ` is a probability measure on the measurable space `(α, Σ)` and `f: α → ℝ∞` is an almost everywhere measurable function with `μ(N) = 0`, then there exists an `x ∈ α\N` such that `f(x) ≤ ∫α f dμ`.
|
MeasureTheory.measure_laverage_le_pos
theorem MeasureTheory.measure_laverage_le_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
μ ≠ 0 → ∫⁻ (a : α), f a ∂μ ≠ ⊤ → 0 < ↑↑μ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}
The theorem, referred to as the "First moment method", states that for any measurable space `α`, any non-zero measure `μ` on this space, and any measurable function `f` from `α` to the extended nonnegative real numbers (which includes [0, ∞]), the function `f` is greater than its mean over a set with a positive measure. More specifically, the measure of the set of points `x` in `α` where the function `f` exceeds its own mean (integrated over the entire space `α` with respect to the measure `μ`) is strictly positive, given that the integral of `f` over `α` is not infinite.
More concisely: For any measurable space `α`, measurable function `f` from `α` to the extended nonnegative real numbers, and finite measure `μ` on `α`, if the integral of `f` over `α` with respect to `μ` is finite and not equal to zero, then the set of points where `f(x) > int(f) dμ` has positive measure.
|
MeasureTheory.laverage_eq_lintegral
theorem MeasureTheory.laverage_eq_lintegral :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α)
[inst : MeasureTheory.IsProbabilityMeasure μ] (f : α → ENNReal), ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
This theorem, named `MeasureTheory.laverage_eq_lintegral`, states that for any type `α`, measurable space `m0` based on `α`, measure `μ` of type `MeasureTheory.Measure α` which is a probability measure (as specified by `MeasureTheory.IsProbabilityMeasure μ`), and a function `f` mapping from `α` to extended nonnegative real numbers (`ENNReal`), the lower Lebesgue integral (denoted by `⨍⁻`) of `f` with respect to `μ` is equal to the Lebesgue integral (denoted by `∫⁻`) of `f` with respect to `μ`.
In terms of mathematical language, it says that for all probability measures `μ` on a measurable space `α`, the lower Lebesgue integral of any function `f : α → [0, ∞]` with respect to `μ` is equal to its Lebesgue integral with respect to `μ`.
More concisely: For any measurable space with a probability measure, the lower Lebesgue integral equals the Lebesgue integral of any measurable function.
|
MeasureTheory.tendsto_integral_smul_of_tendsto_average_norm_sub
theorem MeasureTheory.tendsto_integral_smul_of_tendsto_average_norm_sub :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {ι : Type u_4} {a : ι → Set α} {l : Filter ι} {f : α → E}
{c : E} {g : ι → α → ℝ} (K : ℝ),
Filter.Tendsto (fun i => ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (nhds 0) →
(∀ᶠ (i : ι) in l, MeasureTheory.IntegrableOn f (a i) μ) →
Filter.Tendsto (fun i => ∫ (y : α), g i y ∂μ) l (nhds 1) →
(∀ᶠ (i : ι) in l, Function.support (g i) ⊆ a i) →
(∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / (↑↑μ (a i)).toReal) →
Filter.Tendsto (fun i => ∫ (y : α), g i y • f y ∂μ) l (nhds c)
This theorem, `MeasureTheory.tendsto_integral_smul_of_tendsto_average_norm_sub`, states that for a given function `f` and a sequence of sets `a_i`, if the average of `f` over each set `a_i` converges to a value `c`, then the integral of `f` multiplied by a sequence of functions `g_i` (i.e., `g_i • f`) also tends to `c` under the following conditions:
1. Each `g_i` is supported in corresponding `a_i`, meaning `g_i` only takes non-zero values in `a_i`.
2. The integral of `g_i` converges to 1.
3. The supremum (maximum value) of `g_i` is at most `K / μ a_i`, where `K` is a real constant and `μ a_i` is the measure of the set `a_i`.
In mathematical notation, if $\lim \int_{a_i} \|f(y) - c\| d\mu \to 0$, then $\lim \int g_i(y) f(y) d\mu \to c$ under the above conditions.
More concisely: If for a measurable function $f$ and a sequence of sets $a\_i$ with finite measures, the average of $|f(y) - c|$ over $a\_i$ converges to $0$, and for each $g\_i$ supported in $a\_i$ with integral $1$ and supremum bounded by $K/\mu(a\_i)$, then $\lim \int g\_i(y) f(y) d\mu = c$.
|
MeasureTheory.exists_setAverage_le
theorem MeasureTheory.exists_setAverage_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ},
↑↑μ s ≠ 0 → ↑↑μ s ≠ ⊤ → MeasureTheory.IntegrableOn f s μ → ∃ x ∈ s, ⨍ (a : α) in s, f a ∂μ ≤ f x
This theorem, known as the "First moment method", asserts that for any set `s` of type `α` in a measurable space `α` with measure `μ` and a real-valued function `f` that is integrable on `s` under measure `μ`, given that the measure of the set `s` is neither zero nor infinity, there exists an element `x` in `s` such that the integral average of the function `f` over the set `s` (or the "mean" of `f` over `s`) is less than or equal to the value of the function `f` at `x`. In mathematical terms, this means that the maximum value of an integrable function over a set is greater than or equal to its mean over that set.
More concisely: For any measurable set `s` with finite measure `μ` and integrable function `f` on `α`, there exists an element `x` in `s` such that the integral of `f` over `s` is less than or equal to `f(x)`.
|
MeasureTheory.measure_setAverage_le_pos
theorem MeasureTheory.measure_setAverage_le_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ},
↑↑μ s ≠ 0 → ↑↑μ s ≠ ⊤ → MeasureTheory.IntegrableOn f s μ → 0 < ↑↑μ {x | x ∈ s ∧ ⨍ (a : α) in s, f a ∂μ ≤ f x}
The "First moment method" theorem states that for any set `s` of type `α` in a measurable space with a defined measure `μ`, and any real-valued function `f` that is integrable on this set, given that the measure of the set is not zero and is not infinity, there exists a subset of `s` with positive measure where the function `f` is greater than its mean (defined as the integral of `f` over the set `s`). In other words, if a function is integrable on a set of positive measure, that function must exceed its average value at some points in the set.
More concisely: If `μ(s) > 0` and `∫|f| dμ < ∞` for a measurable set `s` and integrable function `f` in a measurable space with measure `μ`, then there exists a subset `A ⊆ s` with `μ(A) > 0` such that `∫_A f dμ > (∫_s f dμ)`.
|
MeasureTheory.exists_average_le
theorem MeasureTheory.exists_average_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
[inst : MeasureTheory.IsFiniteMeasure μ], μ ≠ 0 → MeasureTheory.Integrable f μ → ∃ x, ⨍ (a : α), f a ∂μ ≤ f x
This theorem, referred to as the "First Moment Method", states that for any given measurable space `α` with a non-zero measure `μ` and an integrable real-valued function `f` defined on `α`, there exists an element `x` in the space such that the mean (average) of `f` over all elements of the space according to measure `μ` is less than or equal to the value of `f` at `x`. In mathematical terms, this is equivalent to saying that there exists an `x` in `α` for which `∫f dμ ≤ f(x)`, where `∫f dμ` denotes the integral of `f` with respect to `μ`, which essentially computes the average of `f` over the space `α`.
More concisely: For any measurable space `(α, μ)` with a non-zero measure and an integrable real-valued function `f`, there exists an element `x` in `α` such that the integral of `f` with respect to `μ` is less than or equal to `f(x)`.
|
MeasureTheory.exists_setLaverage_le
theorem MeasureTheory.exists_setLaverage_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
↑↑μ s ≠ 0 →
MeasureTheory.NullMeasurableSet s μ → ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤ → ∃ x ∈ s, ⨍⁻ (a : α) in s, f a ∂μ ≤ f x
This theorem, known as the "First Moment Method", states that for any measurable space `α`, measure `μ`, and set `s` of `α`, and any function `f` from `α` to the extended non-negative real numbers (denoted by `ENNReal`, which includes the positive infinity), given that the measure of the set `s` is not zero and the set `s` is null measurable (meaning it can be approximated by a measurable set up to a set of null measure), and the integral of function `f` over the set `s` with respect to measure `μ` is not infinite, there exists an element `x` in the set `s` such that the mean (expected value) of `f` over the set `s` is less than or equal to the value of function `f` at `x`.
More concisely: Given a measurable space `(α, μ)`, measurable set `s ≠ ∅`, null measurable `s`, and integrable function `f: α → ENNReal` with finite integral over `s`, there exists an `x ∈ s` such that `∫(s, μ) f ≤ f(x)`.
|
MeasureTheory.exists_not_mem_null_le_integral
theorem MeasureTheory.exists_not_mem_null_le_integral :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ℝ}
[inst : MeasureTheory.IsProbabilityMeasure μ],
MeasureTheory.Integrable f μ → ↑↑μ N = 0 → ∃ x ∉ N, f x ≤ ∫ (a : α), f a ∂μ
The theorem, named as the "First moment method", posits that for a given measurable space 'α', a measure 'μ' on 'α', a set 'N' in 'α', and a real-valued integrable function 'f' on 'α', if 'μ' is a probability measure and the measure of the set 'N' is 0, then there exists an element 'x' in 'α' that is not in 'N' such that the value of the function 'f' at 'x' is less than or equal to the integral of 'f' with respect to 'μ' over the entire space 'α'. In other words, the minimum of an integrable function over a measurable space is less than or equal to the integral of the function over that space, excluding a set of measure zero.
More concisely: If 'μ' is a probability measure on measurable space '(α, Σ)', 'N' ∈ Σ with μ(N) = 0, and 'f' is an integrable real-valued function on 'α', then there exists an x ∈ α \ N such that f(x) ≤ ∫f dμ.
|
MeasureTheory.exists_laverage_le
theorem MeasureTheory.exists_laverage_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
μ ≠ 0 → ∫⁻ (a : α), f a ∂μ ≠ ⊤ → ∃ x, ⨍⁻ (a : α), f a ∂μ ≤ f x
The **First Moment Method** theorem states that for any type `α`, measurable space `m0` of `α`, measure `μ` defined on this space, and a measurable function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), if the measure `μ` is nonzero and the integral of `f` with respect to `μ` is finite, then there exists an element `x` in `α` such that the expected value of `f` (i.e., its mean) is less than or equal to the value of `f` at `x`. In other words, the maximum value of the function `f` is always greater than or equal to its mean.
More concisely: For any measurable function `f` from a nonzero measurable space `(α, mμ)` with finite mean to the extended nonnegative real numbers, there exists an element `x` in `α` such that the mean of `f` is less than or equal to `f(x)`.
|
MeasureTheory.measure_setLaverage_le_pos
theorem MeasureTheory.measure_setLaverage_le_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
↑↑μ s ≠ 0 →
MeasureTheory.NullMeasurableSet s μ →
∫⁻ (a : α) in s, f a ∂μ ≠ ⊤ → 0 < ↑↑μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}
The theorem named "First moment method" states that for any measurable space `α`, a measure `μ` on `α`, a set `s` of `α`, and a measurable function `f` mapping `α` to extended nonnegative real numbers, if the measure of the set `s` is not zero, `s` is a null measurable set under `μ`, and the integral over `s` of `f` with respect to `μ` is not infinite, then there exists a positive measure of the set of elements in `s` for which the function `f` is greater than or equal to its mean over the set `s`. In other words, it asserts that a measurable function exceeds its average value on a set of positive measure.
More concisely: Given a measurable space `α`, a measure `μ`, a measurable set `s` with finite integral of a measurable function `f` greater than its mean over `s`, if `s` is not a null set under `μ`, then there exists a non-empty subset of `s` with positive measure where `f` is greater than or equal to its mean over that subset.
|
MeasureTheory.exists_not_mem_null_lintegral_le
theorem MeasureTheory.exists_not_mem_null_lintegral_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ENNReal}
[inst : MeasureTheory.IsProbabilityMeasure μ],
∫⁻ (a : α), f a ∂μ ≠ ⊤ → ↑↑μ N = 0 → ∃ x ∉ N, ∫⁻ (a : α), f a ∂μ ≤ f x
This theorem, known as the **First Moment Method**, states that for any type `α`, any measurable space `m0` of `α`, any measure `μ` of the measurable space, any set `N` of `α`, and any function `f` from `α` to the extended nonnegative real numbers, if `μ` is a probability measure, the integral of `f` with respect to `μ` is not infinity, and the measure of `N` is 0, then there exists an element `x` in the space but not in `N` such that the integral of `f` over the entire space is less than or equal to the value of `f` at `x`. In other words, there always exists a point outside of a null set where the value of a measurable function is greater than its average over the entire space.
More concisely: For any measurable space with a probability measure, if a measurable function's integral is finite and the measure of its null set is zero, then there exists a point outside of the null set with a function value greater than the function's integral.
|
MeasureTheory.exists_lintegral_le
theorem MeasureTheory.exists_lintegral_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
[inst : MeasureTheory.IsProbabilityMeasure μ], ∫⁻ (a : α), f a ∂μ ≠ ⊤ → ∃ x, ∫⁻ (a : α), f a ∂μ ≤ f x
The theorem, often referred to as the "First moment method", asserts that for any given measurable space `α` with a probability measure `μ`, and any function `f` mapping from `α` to the extended nonnegative real numbers (`ENNReal`), if the Lebesgue integral of `f` with respect to `μ` is not infinity, then there exists an element `x` in the space such that the integral is less than or equal to `f(x)`. In other words, the maximum of a measurable function is always greater than or equal to its integral under these conditions.
More concisely: Given a measurable space `(α, μ)` with a finite integral of a measurable function `f: α → ENNReal`, there exists an element `x ∈ α` such that `∫(α, μ) f dμ ≤ f(x)`.
|
MeasureTheory.exists_not_mem_null_integral_le
theorem MeasureTheory.exists_not_mem_null_integral_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ℝ}
[inst : MeasureTheory.IsProbabilityMeasure μ],
MeasureTheory.Integrable f μ → ↑↑μ N = 0 → ∃ x ∉ N, ∫ (a : α), f a ∂μ ≤ f x
This theorem, often referred to as the "First moment method," asserts that for any measurable space `α`, measure `μ` on `α`, set `N` of `α`, and integrable function `f` mapping `α` to real numbers, if `μ` is a probability measure and the measure of `N` is zero, then there exists an element `x` not in `N` such that the integral of `f` with respect to `μ` is less than or equal to `f(x)`. In other words, the theorem guarantees the existence of a point where the value of `f` exceeds its average (integral), excluding a set of measure zero.
More concisely: Given a measurable space `(α, μ)`, a set `N ⊆ α` with `μ(N) = 0`, and an integrable function `f: α → ℝ`, if `μ` is a probability measure, then there exists an `x ∈ α\N` such that `∫ₕ(f) dμ < f(x)`.
|
MeasureTheory.setAverage_eq
theorem MeasureTheory.setAverage_eq :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
(μ : MeasureTheory.Measure α) (f : α → E) (s : Set α),
⨍ (x : α) in s, f x ∂μ = (↑↑μ s).toReal⁻¹ • ∫ (x : α) in s, f x ∂μ
This theorem, named `MeasureTheory.setAverage_eq`, states that for any type `α`, any normed add commutative group `E` that is also a normed space over the real numbers, a measurable space `m0` on `α`, a measure `μ` on that measurable space, a function `f` from `α` to `E`, and a set `s` of type `α`, the integral of `f` over the set `s` with respect to the measure `μ` is equal to the inverse of the real part of the measure of `s` times the integral of `f` over the set `s` with respect to the measure `μ`. This theorem essentially gives a formula for calculating the average value of a function `f` over a set `s` with respect to a measure `μ` in a measure space.
More concisely: For any measurable space `(α, m0)`, measure `μ`, normed space `(E, ||·||)` over the real numbers, measurable function `f : α → E`, and set `s ⊆ α` with finite measure, the average value of `f` over `s` with respect to `μ` is equal to the inverse of the measure of `s` times the integral of `f` over `s` with respect to `μ`.
|
MeasureTheory.measure_le_laverage_pos
theorem MeasureTheory.measure_le_laverage_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
[inst : MeasureTheory.IsFiniteMeasure μ], μ ≠ 0 → AEMeasurable f μ → 0 < ↑↑μ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}
This theorem is known as the **First Moment Method**. It states that, for any type `α`, any measure space `m0` over `α`, any measure `μ` over `α`, and any function `f` from `α` to the extended nonnegative real numbers, given that the measure `μ` is finite and nonzero, and also that the function `f` is almost everywhere measurable with respect to `μ`, then the measure of the set of all elements `x` for which `f(x)` is less than or equal to the Lebesgue integral of `f` over `μ` is positive. In mathematical terms, if `μ ≠ 0` and `f` is almost everywhere measurable with respect to `μ`, then `0 < μ({x | f(x) ≤ ∫ (a : α), f(a) dμ})`.
More concisely: For any measurable function `f` on a finite and nonzero measure space `(α, μ)`, the set of elements with `f(x)` less than or equal to the Lebesgue integral of `f` has positive measure.
|
MeasureTheory.measure_integral_le_pos
theorem MeasureTheory.measure_integral_le_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
[inst : MeasureTheory.IsProbabilityMeasure μ],
MeasureTheory.Integrable f μ → 0 < ↑↑μ {x | ∫ (a : α), f a ∂μ ≤ f x}
The **First moment method** theorem states that for any integrable function `f` from a measurable space to real numbers, if `μ` is a probability measure on this space, then the measure of the set of points where the function value is greater than or equal to its integral over the space is positive. In mathematical terms, if `f` is integrable with respect to `μ`, then the measure of the set `{x | ∫ (a : α), f a ∂μ ≤ f x}` is greater than zero.
More concisely: If `f` is an integrable function from a measurable space to real numbers with respect to probability measure `μ`, then the measure of the set where `f` exceeds its integral is positive: `μ({x | ∫ (a : α), f a ∂μ ≤ f x}) > 0`.
|
MeasureTheory.exists_not_mem_null_laverage_le
theorem MeasureTheory.exists_not_mem_null_laverage_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ENNReal},
μ ≠ 0 → ∫⁻ (a : α), f a ∂μ ≠ ⊤ → ↑↑μ N = 0 → ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
This theorem, known as the **First Moment Method**, states that for any given type `α`, measurable space `m0`, measure `μ`, set `N`, and function `f` that maps from `α` to the extended nonnegative real numbers, if the measure `μ` is not zero, the Lebesgue integral of `f` with respect to `μ` is not infinity, and the measure of the set `N` is zero, then there exists an element `x` that is not in `N` such that the average (or mean) of `f`, expressed as the Lebesgue integral of `f` with respect to `μ`, is less than or equal to `f(x)`. In simpler terms, the maximum value of a measurable function is greater than its mean, excluding a null set.
More concisely: Given a measurable space `(α, Σ, μ)`, a measurable function `f: α → ℝ∞^+`, and a null set `N ∈ Σ` such that the Lebesgue integral of `f` with respect to `μ` is finite, there exists an element `x ∈ α \ N` with `f(x)` greater than the integral of `f` with respect to `μ`.
|
MeasureTheory.measure_le_setLaverage_pos
theorem MeasureTheory.measure_le_setLaverage_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
↑↑μ s ≠ 0 → ↑↑μ s ≠ ⊤ → AEMeasurable f (μ.restrict s) → 0 < ↑↑μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}
The **First Moment Method** is a theorem in measure theory. It states that for any type `α`, given a measurable space `m0` on `α`, a measure `μ` on `α`, a set `s` of type `α`, and a function `f` from `α` to the extended nonnegative real numbers (ENNReal), if the measure of the set `s` is nonzero and finite, and the function `f` is almost everywhere measurable when restricted to the set `s`, then the measure of the set of elements in `s` where `f` is less than or equal to the mean of `f` over `s` with respect to measure `μ`, is positive. This theorem essentially says that a measurable function is smaller than its mean on a set of positive measure.
More concisely: For any measurable space `(α, m0)`, measure `μ`, set `s` of finite, nonzero measure, and almost everywhere measurable function `f : α → ℝ∞`, the measure of the set `{x ∈ s : f x ≤ ∫s f dμ}` is positive.
|
MeasureTheory.exists_le_setLaverage
theorem MeasureTheory.exists_le_setLaverage :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
↑↑μ s ≠ 0 → ↑↑μ s ≠ ⊤ → AEMeasurable f (μ.restrict s) → ∃ x ∈ s, f x ≤ ⨍⁻ (a : α) in s, f a ∂μ
The theorem, referred to as the "First moment method", asserts that for a given measurable function `f` that maps from a set `s` of some type `α` to the extended nonnegative real numbers (ENNRreal), if the measure of the set `s` is neither zero nor infinity, and the function `f` is almost everywhere measurable on the restriction of a measure `μ` to the set `s`, then there exists an element `x` within the set `s` such that the value of the function `f` at `x` is less than or equal to the mean of the function `f` over the set `s` with respect to the measure `μ`. This theorem is significant in measure theory and is a fundamental result related to the expected value of a measurable function.
More concisely: Given a measurable function `f` from a non-zero, non-complete measure space `(α, Σ, μ)` to the extended nonnegative real numbers, if `f` is almost everywhere defined and integrable, then there exists an element `x` in the domain of `f` such that `∫(s, μ) f dμ ≤ f(x)`.
|
MeasureTheory.exists_integral_le
theorem MeasureTheory.exists_integral_le :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
[inst : MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.Integrable f μ → ∃ x, ∫ (a : α), f a ∂μ ≤ f x
The theorem, termed as the "First moment method", states that for any given measure space defined by the measurable space 'm0' and the measure 'μ', and a real-valued integrable function 'f' defined on this space, if the measure 'μ' is a probability measure, then there exists a point in the space such that the integral of function 'f' over the measure space is less than or equal to the value of function 'f' at that point. In mathematical terms, ∃ x, ∫ (a : α), f a ∂μ ≤ f x. The condition that 'μ' is a probability measure is essential as it normalizes the measure to have total mass one, thereby allowing us to make probabilistic interpretations.
More concisely: Given a measurable space with a probability measure and an integrable function, there exists a point with the property that the integral of the function is less than or equal to its value at that point.
|
MeasureTheory.exists_not_mem_null_le_average
theorem MeasureTheory.exists_not_mem_null_le_average :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ℝ}
[inst : MeasureTheory.IsFiniteMeasure μ],
μ ≠ 0 → MeasureTheory.Integrable f μ → ↑↑μ N = 0 → ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ
This theorem, referred to as the **First Moment Method**, states that for any measure space `α` with a measure `μ`, a set `N` in `α`, and an integrable function `f` from `α` to the real numbers, given that the measure `μ` is finite and not zero and that the measure of `N` is zero, there exists an element `x` in `α` that is not a member of `N` such that the value of `f` at `x` is less than or equal to the mean of the function `f`. In simpler terms, it asserts that the minimum value of an integrable function is not greater than its average, except on a set of measure zero.
More concisely: For any measure space `(α, μ)`, integrable function `f` on `α` with finite and non-zero measure `μ`, and set `N` of measure zero, there exists an `x` in `α \ N` with `f(x) ≤ ∫(α, μ) f dμ / μ(α)`.
|
MeasureTheory.exists_le_lintegral
theorem MeasureTheory.exists_le_lintegral :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
[inst : MeasureTheory.IsProbabilityMeasure μ], AEMeasurable f μ → ∃ x, f x ≤ ∫⁻ (a : α), f a ∂μ
This theorem is known as the "First moment method". It states that for any probability measure space (denoted as 'α', 'm0', and 'μ'), and any extended nonnegative real-valued function ('f') that is almost everywhere measurable with respect to this measure, there exists a point (denoted as 'x') in the space such that the value of the function at this point is less than or equal to the integral of the function with respect to the measure. In mathematical terms, this is saying that the minimum value of a function is always less than or equal to its expected value when interpreted in the context of a probability measure.
More concisely: For any measurable extended real-valued function on a probability measure space and its associated measure, there exists a point in the space where the function's value is less than or equal to the function's integral with respect to the measure.
|
MeasureTheory.exists_le_laverage
theorem MeasureTheory.exists_le_laverage :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
[inst : MeasureTheory.IsFiniteMeasure μ], μ ≠ 0 → AEMeasurable f μ → ∃ x, f x ≤ ⨍⁻ (a : α), f a ∂μ
The **First moment method** theorem states that for any measure space `α` with a non-zero finite measure `μ` and a function `f` from `α` to the extended nonnegative real numbers that is almost everywhere measurable relative to `μ`, there exists a point `x` in the domain of `f` such that the value of `f` at `x` is less than or equal to the "mean" of `f` with respect to the measure `μ`. Here, the "mean" of `f` is defined as the Lebesgue integral of `f` with respect to `μ`, denoted by `⨍⁻ (a : α), f a ∂μ` in Lean.
More concisely: For any measure space `(α, μ)` with a finite, non-zero measure and an almost everywhere measurable function `f` from `α` to the extended nonnegative real numbers, there exists a point `x` in the domain of `f` such that `f x ≤ ∫⁻ a : α, f a dμ`.
|
MeasureTheory.exists_not_mem_null_le_laverage
theorem MeasureTheory.exists_not_mem_null_le_laverage :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ENNReal}
[inst : MeasureTheory.IsFiniteMeasure μ],
μ ≠ 0 → AEMeasurable f μ → ↑↑μ N = 0 → ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
This theorem is known as the "First moment method". It states that for any measurable space `α`, measure `μ`, set `N` and function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), given that `μ` is a finite measure and not equal to 0, and `f` is almost everywhere measurable with respect to `μ`, if the measure of `N` is 0, then there exists an element `x` not in `N` such that `f(x)` is less than or equal to the mean of `f` with respect to `μ`. Essentially, it establishes that the minimum of a measurable function is less than its mean, excluding a null set.
More concisely: Given a measurable space `(α, Σ, μ)`, a finite non-zero measure, an almost everywhere measurable function `f : α → ENNReal`, and a set `N ∈ Σ` with `μ(N) = 0`, there exists an `x ∈ α \ N` such that `f(x) ≤ ∫f dμ`.
|
MeasureTheory.measure_lintegral_le_pos
theorem MeasureTheory.measure_lintegral_le_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
[inst : MeasureTheory.IsProbabilityMeasure μ], ∫⁻ (a : α), f a ∂μ ≠ ⊤ → 0 < ↑↑μ {x | ∫⁻ (a : α), f a ∂μ ≤ f x}
This theorem, known as the "First moment method", is a statement about measurable functions and measures. It states that for any type `α`, measurable space `m0`, measure `μ`, and function `f` from `α` to extended nonnegative real numbers (`ENNReal`), if `μ` is a probability measure, and the Lebesgue integral of `f` with respect to `μ` is not infinite, then there's a positive measure of the set of all `x` from `α` such that the Lebesgue integral of `f` is less than or equal to `f(x)`. In other words, the measure of the set of values for which the function value exceeds its average is positive.
More concisely: If `μ` is a probability measure on measurable space `(α, Σ)`, `f: α → ℝ₁♀∞` is measurable, and the expected value of `f` with respect to `μ` is finite, then there exists a nonempty set `A ∈ Σ` such that `μ(A) > 0` and the essential supremum of `f` on `A` is less than or equal to its expected value.
|
MeasureTheory.exists_le_average
theorem MeasureTheory.exists_le_average :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
[inst : MeasureTheory.IsFiniteMeasure μ], μ ≠ 0 → MeasureTheory.Integrable f μ → ∃ x, f x ≤ ⨍ (a : α), f a ∂μ
This theorem, known as the First Moment Method in measure theory, asserts that given a measurable space and an integrable function defined on it, if the measure is finite and non-zero, then there exists at least one point in the space where the value of the function is less than or equal to the mean (average) of the function across the entire space. In other words, the minimum value of the function does not exceed its mean value. The mean of the function is calculated as the integral of the function with respect to the measure divided by the total measure of the space.
More concisely: Given a measurable space with a finite, non-zero measure and an integrable function on it, the minimum value of the function is less than or equal to its mean value.
|
MeasureTheory.average_neg
theorem MeasureTheory.average_neg :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
(μ : MeasureTheory.Measure α) (f : α → E), ⨍ (x : α), -f x ∂μ = -⨍ (x : α), f x ∂μ
This theorem states that for any measure space `α` and any normed commutative addition group `E` that is a normed space over the real numbers, if we have a measure `μ` on `α` and a function `f` from `α` to `E`, the integral of the negative of `f` with respect to `μ` is equal to the negative of the integral of `f` with respect to `μ`. Essentially, negating a function and then integrating it, or integrating the function first and then negating, yield the same result.
More concisely: For any measure space `α`, any normed commutative addition group `E` over the real numbers, and any function `f` from `α` to `E`, we have `∫(-f) dμ = -∫(f) dμ`.
|
MeasureTheory.measure_average_le_pos
theorem MeasureTheory.measure_average_le_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
[inst : MeasureTheory.IsFiniteMeasure μ],
μ ≠ 0 → MeasureTheory.Integrable f μ → 0 < ↑↑μ {x | ⨍ (a : α), f a ∂μ ≤ f x}
The theorem "MeasureTheory.measure_average_le_pos" is also known as the "First moment method". It states that for any measurable space 'α' with a measure 'μ' and an integrable function 'f' from 'α' to real numbers, if the measure 'μ' is not zero, then there exists a set of positive measure such that 'f' is greater than its average (i.e., its integral divided by the total measure) on this set.
More concisely: For any measurable space '(@alpha, @mu)', integrable function 'f' from 'alpha' to real numbers with non-zero measure 'mu', there exists a measurable set 'A' with positive measure such that the integral of 'f' over 'A' is greater than the average value of 'f'.
|
MeasureTheory.laverage_eq
theorem MeasureTheory.laverage_eq :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
⨍⁻ (x : α), f x ∂μ = (∫⁻ (x : α), f x ∂μ) / ↑↑μ Set.univ
This theorem, named `MeasureTheory.laverage_eq`, states that for any type `α` equipped with a measurable space `m0`, given a measure `μ` on that space and a function `f` mapping from the space to the nonnegative extended real numbers (represented by `ENNReal`), the lower integral (or infimum) of `f` with respect to the measure `μ` is equal to the ratio of the Lebesgue integral of `f` with respect to the measure `μ` and the measure of the entire space `Set.univ` (the universal set on the type `α`). This theorem thus establishes a relationship between the lower integral and the Lebesgue integral of a function in a measurable space.
More concisely: For any measurable space `(α, m0)`, measure `μ`, and measurable function `f : α → ENNReal`, the lower integral of `f` with respect to `μ` equals the Lebesgue integral of `f` divided by the measure of the universal set `Set.univ` in `α` with respect to `m0` and `μ`.
|
MeasureTheory.average_eq
theorem MeasureTheory.average_eq :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
(μ : MeasureTheory.Measure α) (f : α → E), ⨍ (x : α), f x ∂μ = (↑↑μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
The theorem `MeasureTheory.average_eq` states that for any type `α`, `E` with `α` being a measurable space and `E` being a normed add commutative group which is also a normed space over the real numbers, given a measure `μ` on `α` and a function `f` from `α` to `E`, the average value of `f` with respect to `μ` over the entire space `α` (i.e., the universal set `Set.univ`) is equal to the reciprocal of the real value of the total measure of the space `α` times the integral of `f` over the space with respect to `μ`. This essentially represents the concept of weighted average in measure theory.
More concisely: For any measurable space `(α, Σ, μ)`, normed add commutative group `E` with `α` being its carrier set, and integrable function `f` from `α` to `E`, the average value of `f` with respect to `μ` is equal to the integral of `f` multiplied by the reciprocal of the total measure of `α`. In other words, `∫(α, μ, f) = (1 / μ(Set.univ)) * ∑₀(α, μ, f)`.
|
MeasureTheory.measure_le_setAverage_pos
theorem MeasureTheory.measure_le_setAverage_pos :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ},
↑↑μ s ≠ 0 → ↑↑μ s ≠ ⊤ → MeasureTheory.IntegrableOn f s μ → 0 < ↑↑μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ}
This theorem is referred to as the "First Moment Method". It states that for any given set of type `α`, measurable space `m0`, measure `μ`, set `s`, and real-valued function `f`, if the measure of the set `s` is not zero or infinity, and the function `f` is integrable on the set `s` with measure `μ`, then the measure of the subset of `s` where `f` is less than or equal to its average over `s` (computed with respect to `μ`) is positive. This means that an integrable function `f` is smaller than its mean on a set of positive measure.
More concisely: For any measurable set `s` with finite measure and integrable function `f` on `s`, the subset of `s` where `f` is less than or equal to the average of `f` over `s` has positive measure.
|
MeasureTheory.laverage_zero_measure
theorem MeasureTheory.laverage_zero_measure :
∀ {α : Type u_1} {m0 : MeasurableSpace α} (f : α → ENNReal), ⨍⁻ (x : α), f x ∂0 = 0
This theorem states that for any type `α` and a measurable space `m0` of this type, the lower Lebesgue integral (also known as the Lebesgue expectation) of any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`) with respect to the zero measure is always equal to zero. In mathematical terms, we can write this as $\int_{0}^{\infty} f(x) \, d\mu = 0$ where $\mu$ is the zero measure. This means that when we are measuring a function with a measure that assigns zero measure to all sets, the total accumulation (integral) of the function over all elements in the space is zero.
More concisely: For any measurable space with zero measure `m0` and any measurable function `f` from a type `α` to the extended nonnegative real numbers, their lower Lebesgue integral is equal to zero: $\int_{0}^{\infty} f(x) \, d\mu = 0$.
|