MeasureTheory.UniformIntegrable.spec'
theorem MeasureTheory.UniformIntegrable.spec' :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β},
p ≠ 0 →
p ≠ ⊤ →
(∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
MeasureTheory.UniformIntegrable f p μ →
∀ {ε : ℝ},
0 < ε →
∃ C, ∀ (i : ι), MeasureTheory.snorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
This theorem, which is superseded by `UniformIntegrable.spec` that doesn't require measurability, states that for any type `α`, `β`, and `ι`, given a measurable space `α`, a measure `μ` on `α`, a normed add commutative group `β`, a non-extreme (neither `0` nor `∞`) measure `p`, and a family of functions `f` from `ι` to functions from `α` to `β`, if `f` is strongly measurable for every `ι` and uniformly integrable, then for any positive real number `ε`, there exists a constant `C` such that for every `ι`, the seminorm `ℒp` of the function `f` cut off outside the set where the norm of `f` exceeds `C` is at most `ε`. The `ℒp` seminorm is `0` for `p=0`, `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞`, and the essential supremum of `‖f‖` for `p = ∞`. If the real number is negative, `ENNReal.ofReal` returns `0`.
More concisely: For any measurable space `α`, measure `μ`, normed add commutative group `β`, non-extreme measure `p`, and strongly measurable, uniformly integrable family `f` of functions from `ι` to `α` to `β`, there exists a constant `C` such that the `ℒp` seminorm of `f` restricted to the set where the norm of `f` is less than `C` is less than `ε` for every `ε > 0`.
|
MeasureTheory.Memℒp.snorm_indicator_le'
theorem MeasureTheory.Memℒp.snorm_indicator_le' :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{p : ENNReal} {f : α → β},
1 ≤ p →
p ≠ ⊤ →
MeasureTheory.Memℒp f p μ →
MeasureTheory.StronglyMeasurable f →
∀ {ε : ℝ},
0 < ε →
∃ δ,
∃ (_ : 0 < δ),
∀ (s : Set α),
MeasurableSet s →
↑↑μ s ≤ ENNReal.ofReal δ → MeasureTheory.snorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
This theorem, named `MeasureTheory.Memℒp.snorm_indicator_le'`, states that for any types `α` and `β`, a measurable space `α`, a measure `μ` on `α`, a normed add commutative group `β`, a nonnegative extended real number `p` such that `1 ≤ p` and `p ≠ ∞`, a function `f` from `α` to `β` that is almost everywhere strongly measurable and the `p`-seminorm of `f` is finite, and a strongly measurable function `f`, there exists a positive real number `δ` such that for any measurable set `s` whose measure is less than or equal to `δ`, the `p`-seminorm of the indicator function of `s` times `f` is less than or equal to twice `ε`.
Here, an indicator function of a set is a function that takes the value 1 on the set and 0 outside. The `p`-seminorm of a function is a measure of the size of the function, defined differently depending on the value of `p`: it is equal to `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞` and `essSup ‖f‖ μ` for `p = ∞`. The condition that a function `f` is almost everywhere strongly measurable means that it is the limit of simple functions almost everywhere.
More concisely: For any measurable space, measure, normed add commutative group, nonnegative `p`-integrable function `f`, and measurable set `s` with finite measure, there exists a `δ > 0` such that the `p`-seminorm of the product of the indicator function of `s` and `f` is less than or equal to twice the `p`-seminorm of `f`.
|
MeasureTheory.unifIntegrable_const
theorem MeasureTheory.unifIntegrable_const :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal} {g : α → β},
1 ≤ p → p ≠ ⊤ → MeasureTheory.Memℒp g p μ → MeasureTheory.UnifIntegrable (fun x => g) p μ
The theorem `MeasureTheory.unifIntegrable_const` states that, for any types `α`, `β`, and `ι`, measurable space `m`, measure `μ`, normed add commutative group `β`, extended nonnegative real number `p`, and function `g` from `α` to `β`, if `p` is greater than or equal to 1 and is not equal to positive infinity, and the function `g` satisfies the property `MeasureTheory.Memℒp` (which means that `g` is almost everywhere strongly measurable and the norm of `g` raised to the power p and integrated over the measure space is finite if `p` is less than positive infinity, or the essential supremum of `g` is less than positive infinity if `p` equals positive infinity), then the constant function `g` is uniformly integrable.
More concisely: If `α`, `β`, `ι`, measurable space `m`, measure `μ`, normed add commutative group `β`, extended nonnegative real number `p` (`p ≥ 1 ∧ p ≠ ∞`), and function `g` from `α` to `β` satisfy `MeasureTheory.Memℒp`, then the constant function `g` is uniformly integrable with respect to `μ`.
|
MeasureTheory.Memℒp.integral_indicator_norm_ge_nonneg_le_of_meas
theorem MeasureTheory.Memℒp.integral_indicator_norm_ge_nonneg_le_of_meas :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β},
MeasureTheory.Memℒp f 1 μ →
MeasureTheory.StronglyMeasurable f →
∀ {ε : ℝ}, 0 < ε → ∃ M, 0 ≤ M ∧ ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
This theorem states that for any normed additive commutative group `β` and any measurable space `α` with a given measure `μ`, if a function `f: α → β` belongs to the set `L^p` (meaning it is almost everywhere strongly measurable and its `p`-norm is finite) with `p=1`, and if `f` is strongly measurable (meaning it is the limit of simple functions), then for any positive real number `ε`, there exists a nonnegative real number `M` such that the integral of the norm of the indicator function of the set `{x | M ≤ ||f x||₊}` applied to `f` is less than or equal to `ε`. The indicator function here takes the value `f x` for `x` in the set and `0` otherwise.
More concisely: For any normed additive commutative group `β`, measurable space `α` with measure `μ`, and strongly measurable, almost everywhere strongly measurable function `f: α → β` in `L^1`, there exists a nonnegative real number `M` such that the integral of the norm of the indicator function of `{x | M ≤ ||f x||₊}` applied to `f` is less than or equal to `ε`.
|
MeasureTheory.Memℒp.integral_indicator_norm_ge_le
theorem MeasureTheory.Memℒp.integral_indicator_norm_ge_le :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β},
MeasureTheory.Memℒp f 1 μ →
MeasureTheory.StronglyMeasurable f →
∀ {ε : ℝ}, 0 < ε → ∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
The theorem `MeasureTheory.Memℒp.integral_indicator_norm_ge_le` states that for any measurable space `α`, any `NormedAddCommGroup` `β`, a measure `μ` on `α`, and a function `f` from `α` to `β`, if `f` has the property `Memℒp` with parameter `1` (which means `f` is almost everywhere strongly measurable and the `L^1` norm of `f` is finite) and `f` is `StronglyMeasurable` (which means `f` is the limit of simple functions), then for any positive real number `ε`, there exists a real number `M` such that the integral of the nonnegative part of the function `f` at points where its norm is greater or equal to `M`, is less than or equal to `ε`. This theorem provides the `L^1` norm control of the function `f` by a simple function, and the constant `M` depends on `ε`. This theorem is a weaker version of the theorem `MeasureTheory.Memℒp.integral_indicator_norm_ge_nonneg_le` which also provides a nonnegative `M` and does not require the measurability of `f`.
More concisely: Given a measurable space, a Normed Additive Commutative Group, a measure, and a strongly measurable, almost everywhere finite `L^1` function `f` from the measurable space to the group, for any `ε > 0`, there exists a constant `M` such that the integral of the indicator function of the set where `f`'s norm is greater than or equal to `M` is less than or equal to `ε`.
|
MeasureTheory.unifIntegrable_finite
theorem MeasureTheory.unifIntegrable_finite :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal} [inst_1 : Finite ι],
1 ≤ p →
p ≠ ⊤ → ∀ {f : ι → α → β}, (∀ (i : ι), MeasureTheory.Memℒp (f i) p μ) → MeasureTheory.UnifIntegrable f p μ
The theorem `MeasureTheory.unifIntegrable_finite` states that given a measurable space `α`, a normed additive commutative group `β`, a finite type `ι`, a measure `μ` over the space `α`, and a non-infinite extended nonnegative real number `p` greater or equal to 1, if all functions `f : ι → α → β` (from type `ι` to functions from `α` to `β`) are Lp-integrable with respect to the measure `μ`, then these functions are uniformly integrable with respect to the Lp norm. In mathematical terms, for any finite sequence of Lp functions, the integrability of each function in the sequence guarantees the uniform integrability of the sequence.
More concisely: If `α` is a measurable space, `β` is a normed additive commutative group, `ι` is a finite type, `μ` is a measure over `α`, and `p ≥ 1` is a non-infinite extended nonnegative real number, then the family of all `ι`-indexed Lp-integrable functions from `α` to `β` is uniformly integrable.
|
MeasureTheory.Memℒp.snorm_indicator_le_of_meas
theorem MeasureTheory.Memℒp.snorm_indicator_le_of_meas :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{p : ENNReal} {f : α → β},
1 ≤ p →
p ≠ ⊤ →
MeasureTheory.Memℒp f p μ →
MeasureTheory.StronglyMeasurable f →
∀ {ε : ℝ},
0 < ε →
∃ δ,
∃ (_ : 0 < δ),
∀ (s : Set α),
MeasurableSet s →
↑↑μ s ≤ ENNReal.ofReal δ → MeasureTheory.snorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
This theorem states that for any non-negative extended real number `p` that is not infinity and greater than or equal to 1, a measurable space `α`, a normed additive commutative group `β`, a measure `μ` on `α`, and a function `f` from `α` to `β` that is strongly measurable and almost everywhere-strongly measurable with finite `p`-seminorm (`MeasureTheory.Memℒp`), there exists a positive real number `δ` such that for all sets `s` in `α` that are measurable and whose measure is less than or equal to `δ`, the `p`-seminorm of the indicator function of `s` with respect to `f` is less than or equal to any given positive real number `ε`. The theorem further indicates that this result is superseded by `MeasureTheory.Memℒp.snorm_indicator_le`, which does not require `f` to be measurable.
More concisely: For any measurable space `α`, measure `μ`, normed additive commutative group `β`, strongly measurable and almost everywhere-strongly measurable function `f` from `α` to `β` with finite `p`-seminorm, there exists a `δ > 0` such that the `p`-seminorm of the indicator function of any measurable set `s` with measure less than or equal to `δ` is less than `ε`.
|
MeasureTheory.uniformIntegrable_average
theorem MeasureTheory.uniformIntegrable_average :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} {E : Type u_4}
[inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
1 ≤ p →
∀ {f : ℕ → α → E},
MeasureTheory.UniformIntegrable f p μ →
MeasureTheory.UniformIntegrable (fun n => (↑n)⁻¹ • (Finset.range n).sum fun i => f i) p μ
The theorem `MeasureTheory.uniformIntegrable_average` states that for any measure space `α` with a measure `μ`, an extended nonnegative real number `p` greater than or equal to 1, and a sequence of functions `f : ℕ → α → E` from natural numbers to `α` that is uniformly integrable, the sequence obtained by averaging the first `n` elements of `f` is also uniformly integrable. Here, averaging a sequence means dividing the sum of the first `n` elements by `n`, and `E` is a type equipped with a normed addition group structure and a real number normed space structure. In other words, if a sequence of functions is uniformly integrable, then so is the sequence formed by taking the averages of the functions over the first `n` natural numbers.
More concisely: If `α` is a measure space with measure `μ`, `p >= 1` is an extended nonnegative real number, and `f : ℕ → α → E` is a uniformly integrable sequence of functions, then the sequence of averages `n => (∑i
|
MeasureTheory.uniformIntegrable_of
theorem MeasureTheory.uniformIntegrable_of :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
1 ≤ p →
p ≠ ⊤ →
(∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
(∀ (ε : ℝ),
0 < ε →
∃ C, ∀ (i : ι), MeasureTheory.snorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) →
MeasureTheory.UniformIntegrable f p μ
The theorem `MeasureTheory.uniformIntegrable_of` establishes a condition for a sequence of functions `(fₙ)` to be uniformly integrable in the probability sense. It states that for any measure space `α` with measure `μ`, any normed additively commutative group `β`, any type `ι` indexing the sequence of functions `(fₙ)`, and any non-infinite nonnegative real number `p` greater than or equal to 1, if each function `fₙ` is almost everywhere strongly measurable, and for any positive real number `ε`, there exists some constant `C` such that the `p`-seminorm of the indicator function of the set `{x | C ≤ ‖fₙ x‖₊}` (the set of points at which the norm of `fₙ x` is greater than or equal to `C`) is less than or equal to `ε` for all `n`, then the sequence of functions `(fₙ)` is uniformly integrable in the measure theory and probability sense.
More concisely: A sequence of almost everywhere strongly measurable functions `(fₙ : α → β)` is uniformly integrable with respect to a measure `μ` if for any `ε > 0`, there exists a constant `C` such that the integral of the indicator function of `{x | ‖fₙ x‖₊ ≥ C}` is less than `ε` for all `n`.
|
MeasureTheory.uniformIntegrable_subsingleton
theorem MeasureTheory.uniformIntegrable_subsingleton :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β} [inst_1 : Subsingleton ι],
1 ≤ p → p ≠ ⊤ → (∀ (i : ι), MeasureTheory.Memℒp (f i) p μ) → MeasureTheory.UniformIntegrable f p μ
This theorem states that a single function is uniformly integrable in the sense of probability theory. Specifically, given a measurable space `α`, a measure `μ` on `α`, a normed additive commutative group `β`, an extended nonnegative real number `p` such that `1 ≤ p` and `p` is not infinity, and a function `f` from some singleton set `ι` to `β`, if the function `f` satisfies the `MeasureTheory.Memℒp` property (which means it is almost everywhere strongly measurable and the integral of the p-norm of the function is finite or the essential supremum is finite), then `f` is uniformly integrable in the sense of `MeasureTheory.UniformIntegrable` (i.e., each function in the family is almost everywhere strongly measurable, the family is uniformly integrable in the measure theory sense, and there exists a constant such that the p-norm of each function in the family is less than or equal to that constant).
More concisely: Given a measurable space, measure, normed additive commutative group, and a singleton function `f` satisfying the `MeasureTheory.Memℒp` property, `f` is uniformly integrable in the sense of `MeasureTheory.UniformIntegrable`.
|
MeasureTheory.Memℒp.snorm_indicator_norm_ge_pos_le
theorem MeasureTheory.Memℒp.snorm_indicator_norm_ge_pos_le :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{p : ENNReal} {f : α → β},
MeasureTheory.Memℒp f p μ →
MeasureTheory.StronglyMeasurable f →
∀ {ε : ℝ}, 0 < ε → ∃ M, 0 < M ∧ MeasureTheory.snorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
This theorem states that given a nonnegative extended real number `p`, a measure space `α`, a group with a norm `β`, a measure `μ` on the space, and a function `f` from `α` to `β`, if `f` is a member of `ℒp` space (i.e., `f` is almost everywhere strongly measurable and its `ℒp` seminorm is finite) and `f` is strongly measurable (i.e., `f` is the limit of simple functions), then, for any positive real number `ε`, there exists a positive value `M` such that the `ℓp` seminorm of the indicator function that equals `f` when the `ℒp` norm of `f` is greater than or equal to `M` and zero otherwise, is less than or equal to `ε`. This is a result implying that a single function is uniformly integrable in the sense of probability theory.
More concisely: Given a nonnegative extended real number `p`, a measure space `α`, a group with a norm `β`, a measure `μ` on `α`, and a strongly measurable, almost everywhere defined `ℒp` function `f` from `α` to `β` with finite `ℒp` seminorm, there exists a positive number `M` such that the `ℒ1` norm of the indicator function of the set `{x ∈ α | ||f(x)|| > M}` is less than `ε`.
|
MeasureTheory.tendstoInMeasure_iff_tendsto_Lp
theorem MeasureTheory.tendstoInMeasure_iff_tendsto_Lp :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{p : ENNReal} {f : ℕ → α → β} {g : α → β} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
1 ≤ p →
p ≠ ⊤ →
(∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ) →
MeasureTheory.Memℒp g p μ →
(MeasureTheory.TendstoInMeasure μ f Filter.atTop g ∧ MeasureTheory.UnifIntegrable f p μ ↔
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0))
**Vitali's Convergence Theorem**: Given a sequence of functions `f` from natural numbers and a measure space `α` to a normed additive commutative group `β`, the measure `μ` on `α`, and another function `g` from `α` to `β` such that `p` is a nonnegative extended real number with `p` not being infinity and `p` being greater than or equal to 1. If `f` and `g` have the property that they are almost everywhere strongly measurable and their `ℒp` seminorm is finite, then the sequence `f` converges to `g` in the `ℒp` sense if and only if it is uniformly integrable and converges to `g` in measure. In other words, for all `ε > 0`, the measure of the set where the distance between `f` and `g` is greater than or equal to `ε` tends to 0 when `n` goes to infinity and the seminorm of `f(n) - g` tends to 0 in the `ℒp` sense when `n` goes to infinity.
More concisely: Given a sequence of measurable functions `f` from a measure space to a normed additive commutative group, with finite `ℒp` seminorms, if they are almost everywhere convergent to a function `g` and uniformly integrable, then their `ℒp` norms converge to that of `g` as the sequence goes to infinity.
|
MeasureTheory.unifIntegrable_of_tendsto_Lp
theorem MeasureTheory.unifIntegrable_of_tendsto_Lp :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{p : ENNReal} {f : ℕ → α → β} {g : α → β},
1 ≤ p →
p ≠ ⊤ →
(∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ) →
MeasureTheory.Memℒp g p μ →
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0) →
MeasureTheory.UnifIntegrable f p μ
This theorem, titled "Convergence in Lp implies uniform integrability", states that for all measurable spaces `α` and normed additively commutative groups `β`, given a measure `μ` on `α`, an extended nonnegative real number `p` greater than or equal to 1 and not infinity, a sequence of functions `f: ℕ → α → β`, and a function `g : α → β`, if each function in the sequence `f` and the function `g` belong to the Lp space (`MeasureTheory.Memℒp`), and the seminorms (`MeasureTheory.snorm`) of the difference between each function in the sequence `f` and the function `g` tends to 0 (`Filter.Tendsto`) as `n` goes to infinity (`Filter.atTop`), then the sequence of functions `f` is uniformly integrable with respect to `p` and measure `μ` (`MeasureTheory.UnifIntegrable`). In simpler words, the theorem says that if a sequence of functions converges in the Lp norm to a function, then this sequence of functions is uniformly integrable.
More concisely: If a sequence of measurable functions converges to a measurable function in the Lp sense with respect to a measure, then the sequence is uniformly integrable in the Lp sense with respect to that measure.
|
MeasureTheory.tendsto_Lp_of_tendstoInMeasure
theorem MeasureTheory.tendsto_Lp_of_tendstoInMeasure :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{p : ENNReal} {f : ℕ → α → β} {g : α → β} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
1 ≤ p →
p ≠ ⊤ →
(∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
MeasureTheory.Memℒp g p μ →
MeasureTheory.UnifIntegrable f p μ →
MeasureTheory.TendstoInMeasure μ f Filter.atTop g →
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0)
This theorem states the forward direction of Vitali's convergence theorem: if you have a sequence of functions `f` that are uniformly integrable and almost everywhere strongly measurable with respect to a finite measure `μ`, and these functions converge in measure to another function `g` (where convergence in measure is understood with respect to a filter tending towards infinity), then the sequence of functions `f` also converges in Lp to `g`. Here, Lp convergence is defined as the seminorm of the difference between the functions in the sequence and the limit function tending to 0 with respect to a filter tending towards infinity. This theorem requires the condition that `g` belongs to the Lp space for some `p` greater than or equal to 1 but less than infinity.
More concisely: If a sequence of uniformly integrable and almost everywhere measurable functions converges in measure to a function `g` that belongs to the `Lp` space, then the sequence converges in `Lp` to `g`.
|
MeasureTheory.uniformIntegrable_iff
theorem MeasureTheory.uniformIntegrable_iff :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
1 ≤ p →
p ≠ ⊤ →
(MeasureTheory.UniformIntegrable f p μ ↔
(∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) ∧
∀ (ε : ℝ),
0 < ε →
∃ C, ∀ (i : ι), MeasureTheory.snorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε)
This theorem states that the definition of uniform integrability in Lean's mathlib is the same as the definition commonly found in literature. In particular, for a family of measurable functions `f` indexed by `ι`, operating in a measurable space `α` and returning values in a normed addition-commutative group `β`, and given a measure `μ` on `α` and an extended nonnegative real `p` where `1 ≤ p` and `p ≠ ∞`, the condition of uniform integrability is equivalent to two conditions: firstly, each function `f i` is almost everywhere strongly measurable with respect to measure `μ`, and secondly, for any real number `ε` greater than `0`, there exists a constant `C` such that the ℒp seminorm of the function `f i` (restricted to values at which `C ≤ ‖f i x‖₊`) is less than or equal to `ε`. The restriction of the function `f i` is represented by `({x | C ≤ ‖f i x‖₊}.indicator (f i))`, where `indicator` denotes the indicator function.
More concisely: A family of measurable functions from a measurable space to a normed additive commutative group is uniformly integrable with respect to a measure if and only if each function is almost everywhere strongly measurable and for any ε > 0, there exists a constant C such that the ℒp norm of the function restricted to the set where its norm is greater than or equal to C is less than ε.
|
MeasureTheory.unifIntegrable_of'
theorem MeasureTheory.unifIntegrable_of' :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal},
1 ≤ p →
p ≠ ⊤ →
∀ {f : ι → α → β},
(∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
(∀ (ε : ℝ),
0 < ε →
∃ C,
0 < C ∧
∀ (i : ι), MeasureTheory.snorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) →
MeasureTheory.UnifIntegrable f p μ
The theorem `MeasureTheory.unifIntegrable_of'` states that for any measurable space `α`, any normed additively commutative group `β`, any type `ι`, any measure `μ` on `α`, and any extended nonnegative real number `p` such that `1 ≤ p` and `p` is not equal to `∞`, if every function in a family `f : ι → α → β` is `StronglyMeasurable`, and for every positive real `ε` there exists a positive `C` such that the p-semi-norm of the indicator function of the set where `C` is less than or equal to the n-th root of the norm of `f i` is less than or equal to `ε` for every `i`, then the family of functions `f` is uniformly integrable with respect to `p` and `μ`.
In simple terms, this theorem is a condition for a family of functions to be uniformly integrable in terms of measure theory, given some conditions on the p-semi-norm of these functions.
More concisely: Given a measurable space, a normed additively commutative group, a measure, a type, and a Strongly Measurable family of functions to `β` from `ι` to `α` satisfying a condition on their p-semi-norms, these functions are uniformly integrable with respect to the given measure and p-semi-norm.
|
MeasureTheory.tendsto_Lp_of_tendsto_ae_of_meas
theorem MeasureTheory.tendsto_Lp_of_tendsto_ae_of_meas :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{p : ENNReal} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
1 ≤ p →
p ≠ ⊤ →
∀ {f : ℕ → α → β} {g : α → β},
(∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n)) →
MeasureTheory.StronglyMeasurable g →
MeasureTheory.Memℒp g p μ →
MeasureTheory.UnifIntegrable f p μ →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0)
This theorem states that if you have a sequence of functions `(f n)` which are strongly measurable and uniformly integrable, and they converge pointwise almost everywhere (as measured by measure `μ`) to another strongly measurable function `g` which also belongs to the `Lp` space (where `p` is a real number greater than or equal to 1 but not infinity), then the `ℒp` seminorm (a generalization of the `p`-norm) of the difference between the `n`th function in the sequence and `g` tends to 0 as `n` goes to infinity. This essentially means that the sequence of functions `(f n)` converges to `g` in the `Lp` sense, which is a stronger type of convergence than pointwise almost everywhere.
More concisely: If `(f n)` is a sequence of strongly measurable, uniformly integrable functions that converge pointwise almost everywhere to the strongly measurable `Lp` function `g`, then `����f n - g����_p → 0` as `n → ∞`.
|
MeasureTheory.uniformIntegrable_average_real
theorem MeasureTheory.uniformIntegrable_average_real :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal},
1 ≤ p →
∀ {f : ℕ → α → ℝ},
MeasureTheory.UniformIntegrable f p μ →
MeasureTheory.UniformIntegrable (fun n => ((Finset.range n).sum fun i => f i) / ↑n) p μ
This theorem states that if you have a sequence of real-valued functions, `f`, that are uniformly integrable with respect to a measure `μ` and an extended nonnegative real number `p` (where `p` is greater than or equal to 1), then the average of this sequence (obtained by summing over the range of `n` and dividing by `n`) is also uniformly integrable with respect to the same measure `μ` and `p`.
In the context of measure theory and probability theory, this is a key property that ensures that the process of averaging doesn't introduce any additional complexity or irregularity that could cause integrability issues.
More concisely: If `{f_n : ℝ → ℝ}` is a uniformly integrable sequence of real-valued functions with respect to measure `μ` and exponent `p ≥ 1`, then the sequence of averages `(∑i=1^n f_i)/n` is also uniformly integrable with respect to `μ` and `p`.
|
MeasureTheory.uniformIntegrable_const
theorem MeasureTheory.uniformIntegrable_const :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal} {g : α → β},
1 ≤ p → p ≠ ⊤ → MeasureTheory.Memℒp g p μ → MeasureTheory.UniformIntegrable (fun x => g) p μ
This theorem states that a constant sequence of functions is uniformly integrable in the sense of probability theory. Specifically, given a measurable space `α`, a normed add commutative group `β`, an index set `ι`, a measure `μ` on the measurable space, a nonnegative extended real number `p` and a function `g: α → β`, if `p` is greater than or equal to 1 and less than infinity, and if the function `g` belongs to the space `L^p(μ)`, meaning it is almost everywhere strongly measurable and its `p`-th power integral norm is finite, then the constant sequence of functions `(fun x => g)` is uniformly integrable. Uniform integrability here means that all functions in the sequence are almost everywhere strongly measurable, the sequence is uniformly integrable in the measure theory sense, and there exists a constant such that the `p`-th power integral norm of each function in the sequence is less than or equal to this constant.
More concisely: Given a measurable space, a normed add commutative group, an index set, a measure, a nonnegative extended real number `p > 1`, and a function `g` in `L^p(μ)`, the constant sequence `{f(x) = g(x) | x ∈ α}` is uniformly integrable, meaning it is almost everywhere strongly measurable and there exists a constant such that the `p-th` power integral norms of each function are less than or equal to this constant.
|
MeasureTheory.uniformIntegrable_finite
theorem MeasureTheory.uniformIntegrable_finite :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β} [inst_1 : Finite ι],
1 ≤ p → p ≠ ⊤ → (∀ (i : ι), MeasureTheory.Memℒp (f i) p μ) → MeasureTheory.UniformIntegrable f p μ
The theorem `MeasureTheory.uniformIntegrable_finite` states that if we have a finite sequence of functions, each mapping from a measurable space `α` to a normed additive commutative group `β` and indexed by a finite index set `ι`, and each function in this sequence is an Lp function for a given measure `μ` and a non-infinite real number `p` that is greater than or equal to 1, then this sequence of functions is uniformly integrable in the probability sense. Here, an Lp function is a function that is almost everywhere strongly measurable and its norm raised to the power `p` and integrated over the domain is finite. Uniform integrability in this context means that every function in the sequence is almost everywhere strongly measurable, the sequence is uniformly integrable in the measure theory sense, and there exists a constant `C` such that the `p`-th power of the norm of each function in the sequence, integrated with respect to the given measure, is less than or equal to `C`.
More concisely: Given a finite sequence of almost everywhere strongly measurable Lp functions (p ≥ 1) from a measurable space to a normed additive commutative group, their uniform integrability in the probability sense implies the existence of a constant C such that the integral of the p-th power of the norm of each function's absolute value is bounded by C.
|
MeasureTheory.unifIntegrable_subsingleton
theorem MeasureTheory.unifIntegrable_subsingleton :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal} [inst_1 : Subsingleton ι],
1 ≤ p →
p ≠ ⊤ → ∀ {f : ι → α → β}, (∀ (i : ι), MeasureTheory.Memℒp (f i) p μ) → MeasureTheory.UnifIntegrable f p μ
The theorem `MeasureTheory.unifIntegrable_subsingleton` states that given a measurable space `α`, any single function `f` from an index set `ι` to `α` is uniformly integrable for any measure `μ` defined on `α`. This holds under the conditions that `ι` is a singleton set (i.e., a set with exactly one element), `p` is an extended nonnegative real number greater than or equal to 1 and less than infinity, and `f` satisfies the property `MeasureTheory.Memℒp`, meaning it is almost everywhere strongly measurable and its p-th power integral norm is finite. The return type `MeasureTheory.UnifIntegrable f p μ` implies that the function `f` is uniformly integrable with respect to the measure `μ` and the parameter `p`.
More concisely: Given a measurable space `α`, a singleton index set `ι`, a measurable function `f : ι → α` satisfying `MeasureTheory.Memℒp` for some extended nonnegative real number `p ≥ 1`, the function `f` is uniformly integrable with respect to any measure `μ` on `α`.
|
MeasureTheory.tendsto_Lp_of_tendsto_ae
theorem MeasureTheory.tendsto_Lp_of_tendsto_ae :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{p : ENNReal} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
1 ≤ p →
p ≠ ⊤ →
∀ {f : ℕ → α → β} {g : α → β},
(∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
MeasureTheory.Memℒp g p μ →
MeasureTheory.UnifIntegrable f p μ →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0)
This theorem states that, given a sequence of "almost everywhere strongly measurable" functions `f` that are uniformly integrable with respect to measure `μ`, if this sequence converges almost everywhere (μ-a.e.) with respect to `μ` to a function `g` that belongs to Lp space (i.e., `g` is also "almost everywhere strongly measurable" and its Lp norm is finite), then the sequence `f` also converges to `g` in the Lp sense. This is expressed by the requirement that the Lp norm of the difference between `f n` and `g` tends to zero as `n` goes to infinity. The conditions `1 ≤ p` and `p ≠ ⊤` ensure that `p`, the parameter defining the Lp space, is a finite real number greater than or equal to 1.
More concisely: Given a sequence of almost everywhere strongly measurable, uniformly integrable functions `f` with respect to measure `μ` that converge almost everywhere to an almost everywhere strongly measurable `g` in the Lp space (`1 ≤ p < ∞`), the Lp norm of the difference between `fn` and `g` approaches zero as `n` goes to infinity.
|
MeasureTheory.unifIntegrable_fin
theorem MeasureTheory.unifIntegrable_fin :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{p : ENNReal},
1 ≤ p →
p ≠ ⊤ →
∀ {n : ℕ} {f : Fin n → α → β},
(∀ (i : Fin n), MeasureTheory.Memℒp (f i) p μ) → MeasureTheory.UnifIntegrable f p μ
This theorem, `MeasureTheory.unifIntegrable_fin`, states that for any nonnegative real numbers extended with infinity `p` such that `1 ≤ p` and `p` is not infinity, given a measure space `α` with measure `μ`, and a normed additive commutative group `β`, if we have a function `f` indexed by the finite ordinal numbers (up to a natural number `n`), and that for every index `i`, `f i` satisfies the `Memℒp` property (i.e., it is almost everywhere strongly measurable and its pth power integral is finite), then `f` is universally integrable with respect to `p` and `μ`. In mathematical terms, each `f i` is in `L^p(μ)` space and the collection `f` is uniformly integrable.
More concisely: Given a measure space with finite measure, a normed additive commutative group, and a function indexed by finite ordinal numbers whose components are almost everywhere strongly measurable and have finite p-th power integrals for some finite p > 1, the function is uniformly integrable and belongs to L^p.
|
MeasureTheory.uniformIntegrable_of'
theorem MeasureTheory.uniformIntegrable_of' :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
1 ≤ p →
p ≠ ⊤ →
(∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
(∀ (ε : ℝ),
0 < ε →
∃ C, ∀ (i : ι), MeasureTheory.snorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) →
MeasureTheory.UniformIntegrable f p μ
This theorem, which is superseded by `uniformIntegrable_of`, states that for any measurable space `α`, measure `μ`, normed add commutative group `β` and a function `f` mapping from an arbitrary type `ι` to functions from `α` to `β`, given that the measure `μ` is finite, if `p` (an extended non-negative real number) is greater than or equal to `1` and not infinity, and each function `f i` is strongly measurable, then for any positive real number `ε`, there exists a real number `C` such that the seminorm of the indicator function of the set where `C` is less than or equal to the non-negative norm of `f i x`, acting on `f i`, is less than or equal to `ε` when considered as an extended non-negative real number. Under these conditions, the theorem establishes that the family of functions `f` is uniformly integrable with respect to measure `μ` and `p`.
More concisely: Given a measurable space $(\alpha, \mu)$, a normed add commutative group $(\beta, \|.\|)$, a finite measure $\mu$, an extended non-negative real number $p \geq 1$, and a family $f : \ι \to L^p(\alpha, \beta, \mu)$ of strongly measurable functions, the family $f$ is uniformly integrable.
|