MeasureTheory.TendstoInMeasure.congr
theorem MeasureTheory.TendstoInMeasure.congr :
∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Dist E]
{l : Filter ι} {f f' : ι → α → E} {g g' : α → E},
(∀ (i : ι), μ.ae.EventuallyEq (f i) (f' i)) →
μ.ae.EventuallyEq g g' → MeasureTheory.TendstoInMeasure μ f l g → MeasureTheory.TendstoInMeasure μ f' l g'
This theorem states that if a sequence of functions `f` converges in measure to a function `g` with respect to a measure `μ` and a filter `l`, then if `f` and `g` are almost everywhere equal to another sequence of functions `f'` and another function `g'` respectively (with respect to the measure `μ`), then `f'` also converges in measure to `g'` under the same measure `μ` and filter `l`.
In other words, the equality almost everywhere of two sequences of functions and two target functions does not disturb the property of convergence in measure under the given measure and filter.
More concisely: If sequences of functions `f` and `g`, and `f'` and `g'` are almost everywhere equal with respect to a measure `μ`, and `f` converges to `g` in measure under filter `l`, then `f'` converges to `g'` in measure under the same measure `μ` and filter `l`.
|
MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_stronglyMeasurable
theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_stronglyMeasurable :
∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {p : ENNReal} {f : ι → α → E} {g : α → E},
p ≠ 0 →
p ≠ ⊤ →
(∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) →
MeasureTheory.StronglyMeasurable g →
∀ {l : Filter ι},
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) l (nhds 0) →
MeasureTheory.TendstoInMeasure μ f l g
This theorem, `MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_stronglyMeasurable`, states that given a measure space `α` with measure `μ`, a sequence of strongly measurable functions `f : ι → α → E` and a strongly measurable function `g : α → E` in a normed additive commutative group `E`, if the extended nonnegative real number `p` is neither `0` nor `∞`, and if the `ℒp` seminorm of the difference between each function `f n` and `g` tends to `0` for some filter `l` on `ι`, then the sequence of functions `f` converges in measure to the function `g` along the filter `l`. In other words, for any positive real number `ε`, the measure of the set of points where the distance between `f n` and `g` is greater or equal to `ε` tends to `0` as `n` tends to infinity along `l`.
More concisely: Given a measure space, a sequence of strongly measurable functions, a strongly measurable function, and a filter on the index set, if the `ℒp` seminorm of the difference between each function and the limit function tends to 0 for the filter, then the sequence of functions converges in measure to the limit function along the filter.
|
MeasureTheory.tendstoInMeasure_of_tendsto_snorm_top
theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_top :
∀ {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_4}
[inst : NormedAddCommGroup E] {f : ι → α → E} {g : α → E} {l : Filter ι},
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) ⊤ μ) l (nhds 0) → MeasureTheory.TendstoInMeasure μ f l g
This theorem states that for any sequence of functions `f` indexed by `ι`, a measurable space `α`, a measure `μ` on `α`, a function `g` from `α` to a normed additive commutative group `E`, and a filter `l` on `ι`, if the seminorm of the difference between the functions in the sequence `f` and the function `g` tends to 0 in the `l` filter when the `p` in the seminorm is infinity (`⊤`), then the sequence of functions `f` is said to converge in measure to the function `g` along the filter `l`. In other words, for every positive real `ε`, the measure of the set of `α` where the distance between `f i` and `g` is at least `ε` tends to 0 as `i` tends to `l`. This theorem is a special case of the more general theorem `MeasureTheory.tendstoInMeasure_of_tendsto_snorm` which works for all `p ≠ 0` in the seminorm.
More concisely: Given a sequence of measurable functions `f:` ι -> α -> E, a measurable space (α, Σ, μ), a normed additive commutative group E, a function g: α -> E, and a filter l on ι, if the seminorm of f i(x) - g(x) tends to 0 in measure along l as i tends to l, then f converges to g in measure along l.
|
MeasureTheory.tendstoInMeasure_of_tendsto_snorm
theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm :
∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {p : ENNReal} {f : ι → α → E} {g : α → E} {l : Filter ι},
p ≠ 0 →
(∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) →
MeasureTheory.AEStronglyMeasurable g μ →
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) l (nhds 0) →
MeasureTheory.TendstoInMeasure μ f l g
This theorem, "MeasureTheory.tendstoInMeasure_of_tendsto_snorm", states that if a sequence of functions `f` converges to a function `g` in the $L^p$ norm with respect to a measure `μ`, then `f` also converges to `g` in measure. More specifically, if `p` is a non-zero extended nonnegative real number, each function `f_n` in the sequence and the function `g` are almost everywhere strongly measurable with respect to the measure `μ`, and the $L^p$ semi-norm of the difference between `f_n` and `g` tends to zero for the filter `l`, then for any positive real number `ε`, the measure of the set of points where the distance between `f_n(x)` and `g(x)` is greater or equal to `ε` also tends to zero as `n` tends to infinity along the filter `l`. This theorem is a formalization of the fact that convergence in $L^p$ metric implies convergence in measure.
More concisely: If a sequence of almost everywhere strongly measurable functions converges to another function in $L^p$ norm with respect to a measure, then the measure of the sets where the difference between the functions is greater than a given positive constant tends to zero.
|
MeasureTheory.tendstoInMeasure_of_tendsto_Lp
theorem MeasureTheory.tendstoInMeasure_of_tendsto_Lp :
∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {p : ENNReal} [hp : Fact (1 ≤ p)] {f : ι → ↥(MeasureTheory.Lp E p μ)}
{g : ↥(MeasureTheory.Lp E p μ)} {l : Filter ι},
Filter.Tendsto f l (nhds g) → MeasureTheory.TendstoInMeasure μ (fun n => ↑↑(f n)) l ↑↑g
The theorem `MeasureTheory.tendstoInMeasure_of_tendsto_Lp` states that, given a sequence of functions `f` from `ι` to `E` in the `Lp` space and a function `g` in the `Lp` space, if the sequence `f` converges to `g` in the topology of the `Lp` space as `ι` varies along a filter `l`, then the sequence `f` also converges to `g` in measure. In other words, for any `ε > 0`, the measure of the set of `α` where the distance between `f(i)` and `g` is greater than or equal to `ε` tends to zero as `i` converges along the filter `l`. This theorem bridges the concept of convergence in the `Lp` space, a functional analysis concept, with that of convergence in measure, a measure-theoretic concept.
More concisely: If a sequence of functions in the `Lp` space converges to a function in the `Lp` space with respect to the topology of `Lp` space along a filter, then the measure of the set where the sequence's distance from the limit function exceeds a given `ε` tends to zero.
|
MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_ne_top
theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_ne_top :
∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {p : ENNReal} {f : ι → α → E} {g : α → E},
p ≠ 0 →
p ≠ ⊤ →
(∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) →
MeasureTheory.AEStronglyMeasurable g μ →
∀ {l : Filter ι},
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) l (nhds 0) →
MeasureTheory.TendstoInMeasure μ f l g
This theorem, `MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_ne_top`, states that for any measure space `α`, index type `ι`, normed additive commutative group `E`, and measure `μ`, if `p` is a non-zero and non-infinite extended nonnegative real number, and `f` is a sequence of functions from `ι → α → E`, `g` is another function `α → E`, such that for every `n` in `ι`, `f n` is almost everywhere strongly measurable with respect to the measure `μ`, and `g` is also almost everywhere strongly measurable with respect to `μ`, then given any filter `l` on `ι`, if the sequence of ℒp seminorms of the difference between `f n` and `g` converges to 0 with respect to the filter `l`, it follows that the sequence of functions `f` converges in measure to the function `g` with respect to the filter `l`. In other words, for all `ε > 0`, the measure of the set of `x` in `α` such that `ε ≤ dist (f i x) (g x)` tends to 0 as `i` ranges over `ι` and converges along the filter `l`.
More concisely: Given a measure space, a normed additive commutative group, a measure, a non-zero and non-infinite extended nonnegative real number, a sequence of almost everywhere strongly measurable functions, and another almost everywhere strongly measurable function, if the sequence of ℒp seminorms of the difference between the functions converges to 0 with respect to a filter on the index set, then the sequence of functions converges in measure to the other function along the filter.
|
MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable
theorem MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable :
∀ {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MetricSpace E]
{f : ℕ → α → E} {g : α → E} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
(∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n)) →
MeasureTheory.StronglyMeasurable g →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
MeasureTheory.TendstoInMeasure μ f Filter.atTop g
The theorem `MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable` states that for a sequence of functions `{f n}` and a function `g` mapping from a measurable space `α` to a metric space `E`, given a measure `μ` on `α`, if each `f n` and `g` are strongly measurable (meaning they are the limit of simple functions), and almost everywhere with respect to measure `μ`, the sequence `{f n x}` tends to `g(x)` as `n` tends to infinity, then the sequence of functions `{f n}` converges in measure to the function `g`. Here, "converges in measure" means that for every positive value of `ε`, the measure of the set of `x` such that the distance between `f n (x)` and `g(x)` is at least `ε` tends to 0 as `n` tends to infinity.
More concisely: If a sequence of strongly measurable functions `{fn : α → E}` on a measurable space `(α, μ)` converges almost everywhere to a strongly measurable function `g : α → E`, then `{fn}` converges in measure to `g`.
|
MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae
theorem MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae :
∀ {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MetricSpace E]
{f : ℕ → α → E} {g : α → E},
MeasureTheory.TendstoInMeasure μ f Filter.atTop g →
∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => f (ns i) x) Filter.atTop (nhds (g x))
The theorem states that if we have a sequence of functions `f` which converges in measure to a function `g`, then there exists a subsequence of `f` that almost everywhere converges to `g`. In other words, for every measurable space `α`, a measure `μ` on that space, a metric space `E`, and functions `f` from the set of natural numbers and `α` to `E` and `g` from `α` to `E`, if `f` converges in measure to `g`, then there exists a strictly increasing sequence of natural numbers `ns` such that for almost every `x` in `α` (with respect to the measure `μ`), the sequence `f (ns i) x` converges to `g x` as `i` approaches infinity.
More concisely: Given a measurable space `(α, μ)`, a metric space `(E, d)`, and a sequence of functions `f_n : ℕ × α → E` converging in measure to `g : α → E`, there exists a strictly increasing sequence `ns` of natural numbers such that `f_n (ns i) x` converges to `g x` for almost every `x` in `α`.
|
MeasureTheory.tendstoInMeasure_of_tendsto_ae
theorem MeasureTheory.tendstoInMeasure_of_tendsto_ae :
∀ {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MetricSpace E]
{f : ℕ → α → E} {g : α → E} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
(∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
MeasureTheory.TendstoInMeasure μ f Filter.atTop g
The theorem `MeasureTheory.tendstoInMeasure_of_tendsto_ae` states that in a finite measure space, if a sequence of functions `f` is almost everywhere strongly measurable with respect to a measure `μ`, and for almost all `x`, the sequence `f(n, x)` converges to `g(x)` as `n` goes to infinity, then `f` converges in measure to `g`.
In other words, for every `ε > 0`, the measure of the set of `x` such that the distance between `f(n, x)` and `g(x)` is at least `ε`, tends to 0 as `n` goes to infinity. This is a statement about the type of convergence of a sequence of functions in a finite measure space. It's important in measure theory where we are often interested in the limit behaviour of sequences of functions.
More concisely: Given a finite measure space and a sequence of almost everywhere strongly measurable functions `f(n)` converging almost everywhere to `g`, if for each `ε > 0`, the measure of the set where `|f(n) - g| ≥ ε` approaches 0 as `n` goes to infinity, then `f` converges in measure to `g`.
|