MeasureTheory.Martingale.ae_eq_condexp_limitProcess
theorem MeasureTheory.Martingale.ae_eq_condexp_limitProcess :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Martingale f ℱ μ →
MeasureTheory.UniformIntegrable f 1 μ →
∀ (n : ℕ),
μ.ae.EventuallyEq (f n) (MeasureTheory.condexp (↑ℱ n) μ (MeasureTheory.Filtration.limitProcess f ℱ μ))
This theorem, referred to as the part b of the L¹ martingale convergence theorem, states that given a uniformly integrable martingale `f` adapted to the filtration `ℱ`, the function `f` evaluated at any natural number `n` is almost everywhere (a.e.) equal to the conditional expectation of its limiting process with respect to `ℱ n`. Practically, this means that for a martingale `f` and for each time step `n`, the expected value of `f` at that time (given all prior information from the filtration) is equal to the value of `f` itself at that time almost everywhere with respect to the underlying probability measure `μ`. This is a key result in probability theory that underpins the convergence properties of martingales.
More concisely: Given a uniformly integrable martingale `f` adapted to filtration `ℱ`, for each natural number `n`, `f`'s value at `n` is almost everywhere equal to the conditional expectation of its limit with respect to `ℱ_n`.
|
MeasureTheory.Integrable.tendsto_snorm_condexp
theorem MeasureTheory.Integrable.tendsto_snorm_condexp :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
[inst : MeasureTheory.IsFiniteMeasure μ] {g : Ω → ℝ},
MeasureTheory.Integrable g μ →
MeasureTheory.StronglyMeasurable g →
Filter.Tendsto (fun n => MeasureTheory.snorm (MeasureTheory.condexp (↑ℱ n) μ g - g) 1 μ) Filter.atTop
(nhds 0)
This theorem, part c of the L¹ martingale convergence theorem, states that given a function `g` which is integrable and measurable with respect to a filtration `ℱ`, the martingale defined by the conditional expectation of `g` with respect to `ℱ` converges in the L¹ norm to the function `g`. In other words, the L¹ norm (`MeasureTheory.snorm`) of the difference between the conditional expectation of `g` at each step in the filtration and `g` itself, when counted over all natural numbers (`Filter.atTop`), tends towards zero. This convergence also happens almost everywhere, as stated by another result, `MeasureTheory.Integrable.tendsto_ae_condexp`.
More concisely: Given a measurable and integrable function `g` with respect to a filtration `ℱ`, the sequence of conditional expectations of `g` converges to `g` in L¹ norm and almost everywhere.
|
MeasureTheory.Submartingale.ae_tendsto_limitProcess
theorem MeasureTheory.Submartingale.ae_tendsto_limitProcess :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} {R : NNReal} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Submartingale f ℱ μ →
(∀ (n : ℕ), MeasureTheory.snorm (f n) 1 μ ≤ ↑R) →
∀ᵐ (ω : Ω) ∂μ,
Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess f ℱ μ ω))
**Almost Everywhere Martingale Convergence Theorem**: This theorem states that a submartingale `f`, which is a sequence of real-valued functions indexed by natural numbers and is L¹-bounded under a measure `μ`, converges almost everywhere to a function that is measurable with respect to the supremum of a filtration `ℱ`. Here, almost everywhere is with respect to the measure `μ`, which is assumed to be a finite measure. L¹-bounded means that the seminorm (with p=1) of each function in the sequence `f` is less than or equal to a nonnegative real number `R`. The convergence of the submartingale `f` is in the sense that for almost every point `ω`, the limit as `n` tends to infinity (in the filter sense) of the value of the function `f n` at `ω` equals the value of the limit process of the sequence `f` with respect to the filtration `ℱ` at `ω`, where the limit process function is a function from the set Ω to real numbers.
More concisely: A submartingale `f` that is L¹-bounded under a finite measure `μ` converges almost everywhere to a measurable limit function with respect to the supremum filtration `ℱ`.
|
MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd
theorem MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} {R : NNReal} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Submartingale f ℱ μ →
(∀ (n : ℕ), MeasureTheory.snorm (f n) 1 μ ≤ ↑R) →
∀ᵐ (ω : Ω) ∂μ, ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
The theorem `MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd` states that for a L¹-bounded submartingale `f` indexed by the natural numbers under a measure space `Ω` with a measurable space `m0`, a filtration `ℱ`, and a measure `μ`, if every function `f(n)`, for `n` in natural numbers, has its `ℒ1` seminorm (or `ℒ1` norm) less than or equal to a nonnegative real number `R`, then almost everywhere (with respect to the measure `μ`) in `Ω`, there exists a real number `c` such that the sequence `f(n)` converges to `c` as `n` goes to infinity. This theorem essentially says that a L¹-bounded submartingale has a limit almost everywhere.
More concisely: A L¹-bounded submartingale indexed by the natural numbers converges almost everywhere to a real number under a measurable space, measure, and filtration.
|
MeasureTheory.upcrossings_eq_top_of_frequently_lt
theorem MeasureTheory.upcrossings_eq_top_of_frequently_lt :
∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {ω : Ω},
a < b →
(∃ᶠ (n : ℕ) in Filter.atTop, f n ω < a) →
(∃ᶠ (n : ℕ) in Filter.atTop, b < f n ω) → MeasureTheory.upcrossings a b f ω = ⊤
The theorem `MeasureTheory.upcrossings_eq_top_of_frequently_lt` establishes that if a stochastic process, represented by a function `f` from the natural numbers (ℕ) to real numbers (ℝ), frequently visits values below some real number `a` and above some real number `b` (with `a` less than `b`), then the number of upcrossings of the process is infinite. Here, "frequently" is formalized using the filter `Filter.atTop`, which represents the limit towards infinity in an ordered set, and "upcrossings" refer to the number of times the process crosses from below `a` to above `b`.
More concisely: If a stochastic process \(f : \mathbb{N} \to \mathbb{R}\) satisfies \(\exists a < b \in \mathbb{R}. \ f \in \operatorname{Filter.atTop} ([a, b))\), then the number of upcrossings of \(f\) from below \(a\) to above \(b\) is infinite.
|
MeasureTheory.Submartingale.memℒp_limitProcess
theorem MeasureTheory.Submartingale.memℒp_limitProcess :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} {R : NNReal} {p : ENNReal},
MeasureTheory.Submartingale f ℱ μ →
(∀ (n : ℕ), MeasureTheory.snorm (f n) p μ ≤ ↑R) →
MeasureTheory.Memℒp (MeasureTheory.Filtration.limitProcess f ℱ μ) p μ
This theorem states that the limit process of an Lᵖ-bounded submartingale is also Lᵖ. More specifically, given a situation characterized by a measurable space Ω, a measure μ on this space, a filtration ℱ, a sequence of functions (submartingale) `f` mapping natural numbers and elements of Ω to real numbers, a nonnegative real number `R`, and a value `p` in the extended nonnegative real numbers, if `f` is a submartingale of ℱ with respect to μ and the seminorm of `f(n)` for all natural numbers `n` is less than or equal to `R` when measured with respect to `p` and μ, then the limit process of `f` with respect to the filtration ℱ and measure μ is in Lᵖ when measured with respect to `p` and μ. Here, being in Lᵖ means that the function is almost everywhere strongly measurable and its pth power integrable function is finite if `p` is less than infinity, or its essential supremum is finite if `p` is infinity.
More concisely: If `f` is a sub-Martingale with respect to measure `μ` and filtration `ℱ` on measurable space `Ω`, bounded in `Lp(μ)` with constant `R`, then the limit process of `f` is an `Lp(μ)` integrable function.
|
MeasureTheory.tendsto_ae_condexp
theorem MeasureTheory.tendsto_ae_condexp :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
[inst : MeasureTheory.IsFiniteMeasure μ] (g : Ω → ℝ),
∀ᵐ (x : Ω) ∂μ,
Filter.Tendsto (fun n => MeasureTheory.condexp (↑ℱ n) μ g x) Filter.atTop
(nhds (MeasureTheory.condexp (⨆ n, ↑ℱ n) μ g x))
**Lévy's Upward Theorem** in its almost everywhere version states that for a given function `g` and a filtration `ℱ`, the sequence defined by the conditional expectation of `g` given `ℱ n`, denoted as `𝔼[g | ℱ n]`, converges almost everywhere to the conditional expectation of `g` given the supremum of the filtration `ℱ` over `n`, denoted as `𝔼[g | ⨆ n, ℱ n]`. In other words, for almost all points `x` in the underlying measure space `Ω`, the sequence `(MeasureTheory.condexp (↑ℱ n) μ g x)` tends to `(MeasureTheory.condexp (⨆ n, ↑ℱ n) μ g x)` as `n` goes to infinity.
More concisely: For any function `g` and filtration `ℱ`, the sequence of conditional expectations `(𝔼[g | ℱ n])` converges almost everywhere to the conditional expectation `𝔼[g | ⨆ n, ℱ n]` as `n` approaches infinity.
|
MeasureTheory.not_frequently_of_upcrossings_lt_top
theorem MeasureTheory.not_frequently_of_upcrossings_lt_top :
∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {ω : Ω},
a < b →
MeasureTheory.upcrossings a b f ω ≠ ⊤ →
¬((∃ᶠ (n : ℕ) in Filter.atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in Filter.atTop, b < f n ω)
The theorem `MeasureTheory.not_frequently_of_upcrossings_lt_top` states that for any given type Ω, real numbers `a` and `b`, a stochastic function `f` from the natural numbers to `Ω` to the real numbers, and a particular value `ω` in `Ω`, if `a` is less than `b` and the number of upcrossings of the stochastic function from `a` to `b` does not reach infinity for `ω`, then it is not the case that the function frequently returns values less than `a` and greater than `b` as the input natural number approaches infinity. In other words, if a stochastic process frequently crosses from below `a` to above `b`, it will not often visit both ends (`a` and `b`) at the same time.
More concisely: If a stochastic function from the natural numbers to a type Ω with values in the real numbers has finitely many upcrossings from `a` to `b` for some `ω` in Ω and `a < b`, then `ω` does not have arbitrarily long runs of values below `a` and above `b`.
|
MeasureTheory.tendsto_of_uncrossing_lt_top
theorem MeasureTheory.tendsto_of_uncrossing_lt_top :
∀ {Ω : Type u_1} {f : ℕ → Ω → ℝ} {ω : Ω},
Filter.liminf (fun n => ↑‖f n ω‖₊) Filter.atTop < ⊤ →
(∀ (a b : ℚ), a < b → MeasureTheory.upcrossings (↑a) (↑b) f ω < ⊤) →
∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
This theorem, `MeasureTheory.tendsto_of_uncrossing_lt_top`, states that for every type `Ω`, a function `f` from natural numbers to real numbers, and a specific `ω` of type `Ω`, if the liminf (the greatest lower bound) of the norm of the function `f` applied to `n` and `ω` at the filter `atTop` (which represents the limit towards infinity) is less than infinity, and for all rational numbers `a` and `b` where `a` is less than `b`, the number of upcrossings of the function `f` applied to `ω` at rational numbers `a` and `b` is less than infinity, then there exists a real number `c` such that the function `f` applied to `n` and `ω` tends to `c` as `n` goes to infinity (expressed by the `Filter.atTop`). This theorem is essentially about the convergence of a realization of a stochastic process with bounded upcrossings and bounded liminfs.
More concisely: If a real-valued function `f` on natural numbers with domain `Ω` and a point `ω` in `Ω` have finite liminf at `atTop` and finite number of upcrossings for all rational intervals, then `f` converges to some real number `c` as `n` approaches infinity at `ω`.
|
MeasureTheory.Martingale.eq_condexp_of_tendsto_snorm
theorem MeasureTheory.Martingale.eq_condexp_of_tendsto_snorm :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} {g : Ω → ℝ}
{μ : MeasureTheory.Measure Ω},
MeasureTheory.Martingale f ℱ μ →
MeasureTheory.Integrable g μ →
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) 1 μ) Filter.atTop (nhds 0) →
∀ (n : ℕ), μ.ae.EventuallyEq (f n) (MeasureTheory.condexp (↑ℱ n) μ g)
The theorem states that if `f` is a martingale adapted to a filtration `ℱ`, and `f` converges to `g` in the L¹ norm, then for any natural number `n`, the function `f n` is almost everywhere equal to the conditional expectation of `g` given `ℱ n`. Here, "almost everywhere" means except on a set of measure zero. In more mathematical terms, if $f$ is a martingale such that $\|f_n - g\|_1 → 0$ as $n → ∞$, then for all $n$, $f_n = 𝔼[g | \mathcal{F}_n]$ almost surely.
More concisely: Given a martingale $f$ converging to $g$ in $L^1$ norm, for any natural number $n$, $f\_n = 𝔼[g | \mathcal{F}\_n]$ almost surely.
|
MeasureTheory.Integrable.tendsto_ae_condexp
theorem MeasureTheory.Integrable.tendsto_ae_condexp :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
[inst : MeasureTheory.IsFiniteMeasure μ] {g : Ω → ℝ},
MeasureTheory.Integrable g μ →
MeasureTheory.StronglyMeasurable g →
∀ᵐ (x : Ω) ∂μ, Filter.Tendsto (fun n => MeasureTheory.condexp (↑ℱ n) μ g x) Filter.atTop (nhds (g x))
This theorem is part 3 of the L¹ martingale convergence theorem. It states that for a given integrable function `g`, which is measurable with respect to the supremum over `ℱ n` for all `n`, where `ℱ` is a filtration, the martingale defined by the conditional expectation of `g` given `ℱ n`, converges almost everywhere to `g`. In other words, for almost all `x` in the measure space `Ω` under the measure `μ`, and as `n` approaches infinity, the conditional expectation of `g` given `ℱ n` approaches `g(x)`. Furthermore, it's also mentioned that this martingale converges to `g` in the L¹ sense, a result provided by another theorem, `MeasureTheory.Integrable.tendsto_snorm_condexp`.
More concisely: Given a filtration `ℱ`, an integrable and `ℱ_n` measurable function `g`, the sequence of martingales defined by the conditional expectation of `g` with respect to `ℱ_n` converges almost everywhere and in L¹ norm to `g`.
|
MeasureTheory.Submartingale.upcrossings_ae_lt_top'
theorem MeasureTheory.Submartingale.upcrossings_ae_lt_top' :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
{a b : ℝ} {f : ℕ → Ω → ℝ} {R : NNReal} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Submartingale f ℱ μ →
(∀ (n : ℕ), MeasureTheory.snorm (f n) 1 μ ≤ ↑R) →
a < b → ∀ᵐ (ω : Ω) ∂μ, MeasureTheory.upcrossings a b f ω < ⊤
This theorem states that for any submartingale `f` which is L¹-bounded, that is, for all natural numbers `n`, the seminorm of `f(n)` with respect to measure `μ` is less than or equal to some nonnegative real number `R`, the number of upcrossings are almost everywhere bounded for any two real numbers `a` and `b` where `a` is strictly less than `b`. Here, an upcrossing refers to an instance when the stochastic process crosses from below `a` to above `b`. So, essentially, the theorem is saying that if the submartingale is L¹-bounded, then there are hardly any states where the stochastic process crosses from below `a` to above `b` infinitely many times.
More concisely: For any submartingale `f` that is L¹-bounded, the number of upcrossings of real numbers `a` and `b` (where `a < b`) is almost everywhere finite.
|
MeasureTheory.tendsto_snorm_condexp
theorem MeasureTheory.tendsto_snorm_condexp :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
[inst : MeasureTheory.IsFiniteMeasure μ] (g : Ω → ℝ),
Filter.Tendsto
(fun n => MeasureTheory.snorm (MeasureTheory.condexp (↑ℱ n) μ g - MeasureTheory.condexp (⨆ n, ↑ℱ n) μ g) 1 μ)
Filter.atTop (nhds 0)
**Lévy's upward theorem** for L¹ version: This theorem states that given a measurable space `Ω`, a measure `μ` on `Ω`, a filtration `ℱ` (which is a sequence of sub-σ-algebras of `m0`), and a real-valued function `g` defined on `Ω`, the sequence of the L¹ seminorms of the difference between the conditional expectations of `g` with respect to `ℱ n` and `⨆ n, ℱ n` (the supremum of the `ℱ n` as `n` goes to infinity) tends to 0 as `n` goes to infinity. This is to say, for every neighbourhood of 0, there is a natural number `N` such that for all `n >= N`, the L¹ seminorm of the difference between the conditional expectations is in that neighbourhood.
More concisely: Given a measurable space `Ω`, a measure `μ`, a filtration `ℱ`, and a real-valued `g` on `Ω`, the L¹ norm of the difference between `g`'s conditional expectations with respect to `ℱ n` and the supremum of `ℱ n` approaches 0 as `n` increases.
|
MeasureTheory.Submartingale.tendsto_snorm_one_limitProcess
theorem MeasureTheory.Submartingale.tendsto_snorm_one_limitProcess :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ} [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Submartingale f ℱ μ →
MeasureTheory.UniformIntegrable f 1 μ →
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - MeasureTheory.Filtration.limitProcess f ℱ μ) 1 μ)
Filter.atTop (nhds 0)
This theorem is a part of the L¹ martingale convergence theorem. It states that for a uniformly integrable submartingale `f`, which is adapted to a filtration `ℱ`, its sequence of seminorms computed with respect to the difference between `f` at each stage and the limit of the martingale process has a limit of zero. More specifically, as `n` approaches infinity (`Filter.atTop`), the L¹ norm (`MeasureTheory.snorm` with p=1) of the difference between the `n`-th function in the submartingale `f` and the limit process of `f` with respect to `ℱ` and `μ` tends to zero in the neighborhood filter of zero (`nhds 0`). This implies that the submartingale `f` converges almost everywhere and in L¹ to an integrable function that is measurable with respect to the σ-algebra generated by the filtration `ℱ`.
More concisely: Given a uniformly integrable submartingale `f` adapted to filtration `ℱ`, its difference from the limit process converges to zero in L¹ norm as n goes to infinity, implying almost everywhere and L¹ convergence to an integrable, ℱ-measurable limit.
|