MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto
theorem MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} {R : NNReal} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Submartingale f ℱ μ →
(∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
∀ᵐ (ω : Ω) ∂μ,
BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
This theorem, referred to as the "One-sided martingale bound", states that for a given measurable space `Ω` with a measure `μ` and a filtration `ℱ`, if `f` is a submartingale that has uniformly bounded differences, then for almost every `ω` in `Ω`, the function `f n ω` is bounded above (with respect to `n`) if and only if `f n ω` converges as `n` approaches infinity. Here, the bounded differences are determined by a nonnegative real number `R`, and the convergence of `f n ω` is described in terms of a limit `c` where the function `f n ω` tends to `c` when `n` tends to infinity in the topology of the underlying space.
More concisely: For a submartingale `f` with uniformly bounded differences in a measurable space `(Ω, μ, ℱ)`, almost every `ω` in `Ω` satisfies `f n ω` being bounded above (as `n` increases) if and only if `f n ω` converges to some limit `c` as `n` goes to infinity.
|
MeasureTheory.ae_mem_limsup_atTop_iff
theorem MeasureTheory.ae_mem_limsup_atTop_iff :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} (μ : MeasureTheory.Measure Ω)
[inst : MeasureTheory.IsFiniteMeasure μ] {s : ℕ → Set Ω},
(∀ (n : ℕ), MeasurableSet (s n)) →
∀ᵐ (ω : Ω) ∂μ,
ω ∈ Filter.limsup s Filter.atTop ↔
Filter.Tendsto
(fun n => (Finset.range n).sum fun k => MeasureTheory.condexp (↑ℱ k) μ ((s (k + 1)).indicator 1) ω)
Filter.atTop Filter.atTop
**Lévy's generalization of the Borel-Cantelli lemma**: This theorem states that, given a sequence of sets `s` and a filtration `ℱ` such that each set `s n` in the sequence is `ℱ n`-measurable, the upper limit (`limsup`) of `s` as it approaches infinity is almost everywhere equal to the set for which the sum of the conditional probability of `s (k + 1)` given `ℱ k` is infinite. In other words, for almost every event `ω`, `ω` belongs to the `limsup` of `s` at infinity if and only if, as `n` approaches infinity, the sum of the conditional expectations of the indicator function of `s (k + 1)` (which is 1 for each `k` in the range of `n`) tends to infinity.
More concisely: For a sequence of `ℱ`-measurable sets `s`, the set `ω` belongs to the limsup of `s` if and only if the conditional sum of indicators `∑ₙ ℙ(s_(k+1) | ℱ\_k)` diverges almost everywhere.
|
MeasureTheory.Submartingale.exists_tendsto_of_abs_bddAbove_aux
theorem MeasureTheory.Submartingale.exists_tendsto_of_abs_bddAbove_aux :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} {R : NNReal} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Submartingale f ℱ μ →
f 0 = 0 →
(∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
∀ᵐ (ω : Ω) ∂μ,
BddAbove (Set.range fun n => f n ω) → ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
This theorem, which is superseded by `Submartingale.bddAbove_iff_exists_tendsto`, states that for a measurable space $\Omega$ with a measure $\mu$ and a filtration $\mathcal{F}$ on $\Omega$, if a function $f:\mathbb{N} \rightarrow \Omega \rightarrow \mathbb{R}$ is a submartingale and $f$ at 0 equals 0, and almost everywhere in $\Omega$ with respect to the measure $\mu$, the absolute difference between $f(i + 1)$ and $f(i)$ does not exceed a nonnegative real number $R$, then it holds that almost everywhere in $\Omega$ with respect to the measure $\mu$, if the set of values that $f$ takes on is bounded above, there exists a real number $c$ such that $f(n)$ tends to $c$ as $n$ tends to infinity.
More concisely: If $f:\mathbb{N} \rightarrow \Omega \rightarrow \mathbb{R}$ is a submartingale on the measurable space $(\Omega, \mathcal{F}, \mu)$ with $f(0) = 0$ almost everywhere, and for some $R \ge 0$, $|f(i+1)(x) - f(i)(x)| \le R$ almost everywhere for all $i \in \mathbb{N}$ and $x \in \Omega$, then $f$ is almost surely bounded above, and there exists a real number $c$ such that $f(n) \rightarrow c$ as $n \rightarrow \infty$.
|
MeasureTheory.tendsto_sum_indicator_atTop_iff
theorem MeasureTheory.tendsto_sum_indicator_atTop_iff :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} {R : NNReal} [inst : MeasureTheory.IsFiniteMeasure μ],
(∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω) →
MeasureTheory.Adapted ℱ f →
(∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
(∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R) →
∀ᵐ (ω : Ω) ∂μ,
Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atTop ↔
Filter.Tendsto (fun n => MeasureTheory.predictablePart f ℱ μ n ω) Filter.atTop Filter.atTop
This theorem states that for a given measurable space `Ω` with a measure `μ` and a filtration `ℱ` on `Ω`, along with a sequence of functions `f` from the natural numbers and `Ω` to the real numbers and a nonnegative real number `R`, under the assumption that `μ` is a finite measure, the theorem asserts the following:
If almost everywhere with respect to `μ`, the sequence `f` is monotone (i.e., `f n ω ≤ f (n + 1) ω` for all `n`), `f` is adapted to the filtration `ℱ`, each function `f n` is integrable with respect to `μ`, and the differences between successive values of `f` (i.e., `|f (n + 1) ω - f n ω|`) are always less than or equal to `R`, then for almost every `ω`, the function `f n ω` tends to positive infinity as `n` tends to infinity if and only if the predictable part of `f` with respect to `ℱ` and `μ` also tends to positive infinity as `n` tends to infinity. This is represented in Lean as `Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atTop` and `Filter.Tendsto (fun n => MeasureTheory.predictablePart f ℱ μ n ω) Filter.atTop Filter.atTop` respectively.
More concisely: Given a measurable space `Ω` with a finite measure `μ` and a filtration `ℱ`, if a monotone, adapted sequence `f` of integrable functions with difference bounds `R` has almost everywhere increasing values tending to infinity, then its predictable part also tends to infinity almost everywhere.
|