MeasureTheory.martingale_iff
theorem MeasureTheory.martingale_iff :
∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : ι → Ω → E} {ℱ : MeasureTheory.Filtration ι m0} [inst_4 : PartialOrder E],
MeasureTheory.Martingale f ℱ μ ↔ MeasureTheory.Supermartingale f ℱ μ ∧ MeasureTheory.Submartingale f ℱ μ
This theorem, `MeasureTheory.martingale_iff`, defines the condition under which a stochastic process is a martingale. For any types `Ω`, `E`, and `ι`, with `Ω` being a measurable space and `μ` its measure, `E` being a normed add commutative group also being a complete normed space over the reals, and `ι` being a preordered type representing time, and given a stochastic process `f` (a function from time `ι` to a function from `Ω` to `E`) and a filtration `ℱ` (a sequence of sigma-algebras representing the information available at each time), the process `f` is a martingale if and only if it is both a supermartingale and a submartingale.
More concisely: A stochastic process is a martingale if and only if it is both a supermartingale and a submartingale.
|
MeasureTheory.Submartingale.stronglyMeasurable
theorem MeasureTheory.Submartingale.stronglyMeasurable :
∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : ι → Ω → E} {ℱ : MeasureTheory.Filtration ι m0} [inst_4 : LE E],
MeasureTheory.Submartingale f ℱ μ → ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)
The theorem `MeasureTheory.Submartingale.stronglyMeasurable` states that for any pre-ordered set `ι`, a measure space `Ω`, a measure `μ` on `Ω`, a normed, ordered, complete vector space `E` over the real numbers, a function `f` from `ι` to `Ω → E`, and a filtration `ℱ` of the measure space `Ω` indexed by `ι`, if `f` is a submartingale with respect to the filtration `ℱ` and the measure `μ`, then for every index `i` in `ι`, the function `f i` mapping `Ω` to `E` is strongly measurable. Here, a function is said to be strongly measurable if it can be approximated by a sequence of simple functions.
More concisely: If a function `f` is a submartingale with respect to a filtration `ℱ` and measure `μ` on a measure space `Ω` over a normed, ordered, complete vector space `E`, then for each index `i` in `ι`, the function `fi` is strongly measurable.
|
MeasureTheory.Submartingale.sum_mul_sub
theorem MeasureTheory.Submartingale.sum_mul_sub :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
[inst : MeasureTheory.IsFiniteMeasure μ] {R : ℝ} {ξ f : ℕ → Ω → ℝ},
MeasureTheory.Submartingale f 𝒢 μ →
MeasureTheory.Adapted 𝒢 ξ →
(∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R) →
(∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω) →
MeasureTheory.Submartingale (fun n => (Finset.range n).sum fun k => ξ k * (f (k + 1) - f k)) 𝒢 μ
This theorem states that for any measurable space `Ω`, filtration `𝒢` indexed by natural numbers on `Ω`, finite measure `μ` on `Ω`, and real number `R`, if a sequence of functions `f` is a submartingale with respect to `𝒢` and `μ`, and another sequence of functions `ξ` is adapted to `𝒢`, with each `ξ n ω` being nonnegative and less than or equal to `R`, then the sequence of functions defined by the sum (over `k` ranging from 0 to `n-1`) of the product of `ξ k` and the difference `f (k + 1) - f k` is also a submartingale with respect to `𝒢` and `μ`. In mathematical terms, this is saying that a weighted sum of differences of a submartingale is also a submartingale.
More concisely: If `{f}` is a submartingale, `{ξ}` is an adapted sequence of nonnegative functions with `ξ n ω ≤ R` for all `n` and `ω`, then the sequence `{g_n}` defined by `g_n = ∑ⁱ₋₁ i=0 (ξ_i * (f_(i+1) - f_i))` is also a submartingale.
|
MeasureTheory.Martingale.submartingale
theorem MeasureTheory.Martingale.submartingale :
∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : ι → Ω → E} {ℱ : MeasureTheory.Filtration ι m0} [inst_4 : Preorder E],
MeasureTheory.Martingale f ℱ μ → MeasureTheory.Submartingale f ℱ μ
This theorem states that, given a particular set of conditions, if a function `f` is a martingale with respect to a filtration `ℱ` and a measure `μ`, then `f` is also a submartingale with the same `ℱ` and `μ`. The conditions include: the function `f` mapping from a type `ι` to a space of type `E` that is a normed add commutative group, a normed space over the real numbers, and a complete space; `ℱ` being a filtration over a measurable space of type `Ω` that `f` maps to; and `E` and `ι` both having a preorder. In the context of probability theory, a martingale is a sequence of random variables where the expected value of the next variable, given all past variables, is equal to the present variable. A submartingale is a sequence of random variables where the expected value of the next variable, given all past variables, is greater than or equal to the present variable.
More concisely: If `f` is a martingale with respect to filtration `ℱ` and measure `μ` on a measurable space `Ω`, and `f` maps to a normed add commutative group `E` over the real numbers that is complete, then `f` is a submartingale with the same filtration `ℱ` and measure `μ`.
|
MeasureTheory.Submartingale.adapted
theorem MeasureTheory.Submartingale.adapted :
∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : ι → Ω → E} {ℱ : MeasureTheory.Filtration ι m0} [inst_4 : LE E],
MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Adapted ℱ f
The theorem `MeasureTheory.Submartingale.adapted` states that for any type of event space `Ω`, any type of expected value `E`, any type of index `ι` with a preorder structure, a measurable space `m0`, a measure `μ` on this space, a normed add commutative group structure and normed space structure over the real numbers `ℝ` on `E`, and complete space structure on `E`, if `f` is a submartingale with respect to a filtration `ℱ` and measure `μ`, then `f` is adapted to the filtration `ℱ`. Here, `f` being a submartingale means it is a type of stochastic process that has the property of having an expected value that is greater than or equal to the previous expected value, given the past events. Being adapted to the filtration means that for all `i`, `f i` is `ℱ i`-measurable, i.e., `f i` respects the σ-algebra structure of `ℱ i`.
More concisely: If `f` is a submartingale with respect to a filtration `ℱ` and measure `μ` over a measurable space `(Ω, Σ)` with a complete normed add commutative group and normed space structure over the real numbers, then `f` is adapted to `ℱ`, i.e., `f i` is `ℱ i`-measurable for all indices `i`.
|
MeasureTheory.Martingale.eq_zero_of_predictable
theorem MeasureTheory.Martingale.eq_zero_of_predictable :
∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {𝒢 : MeasureTheory.Filtration ℕ m0}
[inst_3 : MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
MeasureTheory.Martingale f 𝒢 μ →
(MeasureTheory.Adapted 𝒢 fun n => f (n + 1)) → ∀ (n : ℕ), μ.ae.EventuallyEq (f n) (f 0)
The theorem `MeasureTheory.Martingale.eq_zero_of_predictable` states that, for a given type of outcome `Ω`, a type `E` which is a complete normed additive commutative group and also a real normed space, a `measurable space` over `Ω`, a `measure` over `Ω`, a `filtration` over the `measurable space`, and a sequence of functions `f` from natural numbers to functions from `Ω` to `E`, if `f` is a martingale with respect to the filtration and the measure, and `f` (shifted by one index) is adapted to the filtration, then for all natural numbers `n`, `f n` is almost everywhere equal to `f 0`. That is, with probability 1, the value of `f` at any time `n` in the future is equal to its initial value. This characterizes the martingale property of fairness over time, where the expected future value of the function does not change with time.
More concisely: If `f` is a martingale with respect to a measure and filtration such that `f` and its shift are adapted, then almost everywhere, `fn = f0`.
|
MeasureTheory.Submartingale.integrable
theorem MeasureTheory.Submartingale.integrable :
∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : ι → Ω → E} {ℱ : MeasureTheory.Filtration ι m0} [inst_4 : LE E],
MeasureTheory.Submartingale f ℱ μ → ∀ (i : ι), MeasureTheory.Integrable (f i) μ
The theorem states that for any submartingale `f` indexed by a preorder `ι` and defined on a given measurable space `Ω` with a measure `μ`, measurement filtration `ℱ`, and values in a real normed, complete additive group `E` with a partial order, each function `f i` (for every `i` in `ι`) is integrable. In mathematical terms, integrability here means that each `f i` is measurable and the integral of the norm of `f i` with respect to the measure `μ` is finite.
More concisely: For any submartingale `f` indexed by a preorder `ι` on measurable space `(Ω, ℱ, μ)` with values in a real normed, complete additive group `(E, ≤)`, each function `fi` is integrable, i.e., measurable and ∫ |fi|dμ<∞.
|
MeasureTheory.submartingale_of_set_integral_le_succ
theorem MeasureTheory.submartingale_of_set_integral_le_succ :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
[inst : MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → ℝ},
MeasureTheory.Adapted 𝒢 f →
(∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
(∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ) →
MeasureTheory.Submartingale f 𝒢 μ
The theorem `MeasureTheory.submartingale_of_set_integral_le_succ` states the following in plain English:
Given a type `Ω` with a `measurable space` structure `m0` and a measure `μ`, along with a filtration `𝒢` over the natural numbers in `m0` and a sequence of functions `f` from the natural numbers to real-valued functions on `Ω`, if `f` is adapted to `𝒢` (meaning that each `f i` is `𝒢 i`-measurable), and each `f i` is integrable with respect to `μ`, and for every natural number `i` and measurable set `s`, the integral of `f i` over `s` is less than or equal to the integral of `f (i+1)` over `s`, then `f` is a submartingale with respect to `𝒢` and `μ`.
In mathematical terms, this theorem is about the property of submartingales, which are sequences of random variables or functions that have the property that the expected value of the next term in the sequence, given all the previous terms, is less than or equal to the current term.
More concisely: If `Ω` is a measurable space with measure `μ`, `𝒢` is a filtration over the natural numbers in `m0`, `f` is an adapted, integrable sequence of real-valued `𝒢`-measurable functions on `Ω` such that for all `i` and measurable sets `s`, `∫(s, μ) (fi) ≤ ∫(s, μ) (f (i+1)),` then `f` is a submartingale with respect to `𝒢` and `μ`.
|
MeasureTheory.Martingale.supermartingale
theorem MeasureTheory.Martingale.supermartingale :
∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : ι → Ω → E} {ℱ : MeasureTheory.Filtration ι m0} [inst_4 : Preorder E],
MeasureTheory.Martingale f ℱ μ → MeasureTheory.Supermartingale f ℱ μ
This theorem states that for any martingale `f`, given the conditions of a set `Ω`, a normed additive commutative group `E`, a complete space `E`, a preorder on `ι`, a filtration `ℱ` on `ι`, a measure `μ` on `Ω`, and a preorder on `E`, the martingale `f` is also a supermartingale. Here, Ω is the set of possible outcomes, E is the set of real numbers (or a subset of the real numbers) representing the possible values of the martingale, and ι is an indexing type representing time in the martingale process. A martingale is a model of a fair game where knowledge of past events never helps predict the mean of the future winnings, and a supermartingale is a model where the expected value of the future values is less than or equal to the current value.
More concisely: For any martingale `f` on a complete space `(Ω, ℱ, μ)` with values in a normed additive commutative group `E` and a preorder, `f` is also a supermartingale.
|
MeasureTheory.Submartingale.sum_mul_sub'
theorem MeasureTheory.Submartingale.sum_mul_sub' :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
[inst : MeasureTheory.IsFiniteMeasure μ] {R : ℝ} {ξ f : ℕ → Ω → ℝ},
MeasureTheory.Submartingale f 𝒢 μ →
(MeasureTheory.Adapted 𝒢 fun n => ξ (n + 1)) →
(∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R) →
(∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω) →
MeasureTheory.Submartingale (fun n => (Finset.range n).sum fun k => ξ (k + 1) * (f (k + 1) - f k)) 𝒢 μ
This theorem states that given a discrete submartingale `f` and a predictable process `ξ` (which means that `ξ (n + 1)` is adapted to a filtration `𝒢`), the process defined by `fun n => ∑ k in Finset.range n, ξ (k + 1) * (f (k + 1) - f k)` is also a submartingale. This holds under the conditions that the measure `μ` is finite, `ξ n ω` is always less than or equal to some real number `R` for all natural numbers `n` and all possible values `ω` of our outcome space `Ω`, and `ξ n ω` is always non-negative.
More concisely: Given a discrete submartingale `f` and a predictable process `ξ` with finite measure `μ`, such that `ξ` is bounded by some real number `R` and is non-negative, the process defined by `sum (k in range (n), ξ (k + 1) * (f (k + 1) - f k))` is also a submartingale.
|
MeasureTheory.Submartingale.zero_le_of_predictable
theorem MeasureTheory.Submartingale.zero_le_of_predictable :
∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {𝒢 : MeasureTheory.Filtration ℕ m0} [inst_3 : Preorder E]
[inst_4 : MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
MeasureTheory.Submartingale f 𝒢 μ →
(MeasureTheory.Adapted 𝒢 fun n => f (n + 1)) → ∀ (n : ℕ), μ.ae.EventuallyLE (f 0) (f n)
The theorem `MeasureTheory.Submartingale.zero_le_of_predictable` states that for all measurable spaces `Ω`, normed additive commutative groups `E`, measure spaces `μ` on `Ω`, filtrations `𝒢` of `Ω` and sequences of functions `f : ℕ → Ω → E`, if `f` is a submartingale with respect to `𝒢` and `μ`, and the sequence of functions `f (n + 1)` is adapted to the filtration `𝒢`, then for every natural number `n`, the function `f 0` is almost surely less or equal to the function `f n`. In simple terms, a predictable submartingale is almost surely greater or equal to its initial state.
More concisely: For any measurable spaces Ω, normed additive commutative groups E, measure spaces μ on Ω, filtrations 𝒢 of Ω, and a submartingale f : ℕ → Ω → E with respect to 𝒢 and μ, if f(n+1) is 𝒢-adapted, then almost surely, f(0) ≤ f(n).
|
MeasureTheory.Supermartingale.le_zero_of_predictable
theorem MeasureTheory.Supermartingale.le_zero_of_predictable :
∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {𝒢 : MeasureTheory.Filtration ℕ m0} [inst_3 : Preorder E]
[inst_4 : MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
MeasureTheory.Supermartingale f 𝒢 μ →
(MeasureTheory.Adapted 𝒢 fun n => f (n + 1)) → ∀ (n : ℕ), μ.ae.EventuallyLE (f n) (f 0)
The given theorem states that for any measure space `Ω` with a measure `μ`, and any normed and complete additive commutative group `E` under the real number field, given a filtration `𝒢` of the natural numbers `ℕ` over the space `Ω`, if function `f : ℕ → Ω → E` is a supermartingale with respect to `𝒢` and `μ`, and if `f` adapted to `𝒢` (i.e., `f (n + 1)` is measurable for all `n`), then for every natural number `n`, almost everywhere in the measure space `Ω`, the value of `f n` is less than or equal to the initial value of `f`, that is, `f 0`. In other words, a predictable supermartingale is almost everywhere less than or equal to its initial state.
More concisely: If `Ω` is a measure space with measure `μ`, `E` is a normed and complete additive commutative group under real numbers, `𝒢` is a filtration of natural numbers over `Ω`, `f : ℕ → Ω → E` is a supermartingale and adapted to `𝒢`, then almost everywhere in `Ω`, `∀n, f n ≤ f 0`.
|
MeasureTheory.Martingale.condexp_ae_eq
theorem MeasureTheory.Martingale.condexp_ae_eq :
∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : ι → Ω → E} {ℱ : MeasureTheory.Filtration ι m0},
MeasureTheory.Martingale f ℱ μ →
∀ {i j : ι}, i ≤ j → μ.ae.EventuallyEq (MeasureTheory.condexp (↑ℱ i) μ (f j)) (f i)
The theorem `MeasureTheory.Martingale.condexp_ae_eq` states that for any given `Ω`, `E`, and `ι` types, where `Ω` is a measurable space, `E` is a normed add-commutative group and a normed space over reals that is also complete, and `ι` is a preorder, and for any given measure `μ` on `Ω`, filtration `ℱ` and `f` which is a martingale with respect to `ℱ` and `μ`, the following holds: for all `i` and `j` in `ι` such that `i` is less than or equal to `j`, the conditional expectation of `f j` with respect to the `i`-th σ-algebra in the filtration `ℱ` is almost everywhere equal to `f i` under the measure `μ`. The "almost everywhere" here refers to the set of points where the equality holds, has the complement set with measure zero.
More concisely: For any measure space `(Ω, ℱ, μ)`, normed add-commutative group and normed space `E` over reals that is complete, preorder `ι`, and martingale `f` with respect to filtration `ℱ` and measure `μ`: The conditional expectation of `f j` with respect to the `i`-th σ-algebra is almost everywhere equal to `f i`, where the equality holds for a set with complement having measure zero.
|
MeasureTheory.submartingale_nat
theorem MeasureTheory.submartingale_nat :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
[inst : MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → ℝ},
MeasureTheory.Adapted 𝒢 f →
(∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
(∀ (i : ℕ), μ.ae.EventuallyLE (f i) (MeasureTheory.condexp (↑𝒢 i) μ (f (i + 1)))) →
MeasureTheory.Submartingale f 𝒢 μ
The theorem `MeasureTheory.submartingale_nat` states that for a given measure space `Ω` with an associated measurable space `m0` and measure `μ`, along with a filtration `𝒢` of `m0` with respect to natural numbers and assuming that the measure `μ` is finite, if we have a sequence of functions `f` from natural numbers to `Ω` that is adapted to the filtration `𝒢` (meaning each function in the sequence is strongly measurable under the particular filtration), and each function in the sequence is integrable with respect to the measure `μ`, and for each natural number `i`, almost everywhere according to the measure `μ`, the function at index `i` in the sequence is less than or equal to the conditional expectation of the function at index `i + 1` with respect to the `i`th filtration and measure `μ`, then this sequence of functions `f` is a submartingale under filtration `𝒢` and measure `μ`. A submartingale is a sequence of random variables or functions that has the property that the expected value of the next term in the sequence, given all previous terms, is greater than or equal to the value of the current term.
More concisely: If `Ω` is a measure space with finite measure `μ`, `𝒢` is a filtration of measurable space `m0`, and `f` is a sequence of strongly measurable, integrable functions adapted to `𝒢` such that almost everywhere `μ`, each `fi` is less than or equal to the conditional expectation of `f(i+1)` given `𝒢(i)` and `μ`, then `f` is a submartingale under filtration `𝒢` and measure `μ`.
|
MeasureTheory.submartingale_of_condexp_sub_nonneg_nat
theorem MeasureTheory.submartingale_of_condexp_sub_nonneg_nat :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
[inst : MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → ℝ},
MeasureTheory.Adapted 𝒢 f →
(∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
(∀ (i : ℕ), μ.ae.EventuallyLE 0 (MeasureTheory.condexp (↑𝒢 i) μ (f (i + 1) - f i))) →
MeasureTheory.Submartingale f 𝒢 μ
This theorem states that for any type `Ω` with a measurable space `m0`, a measure `μ`, a filtration `𝒢` over natural numbers on `m0`, and a sequence of functions `f` from natural numbers to `Ω` mapped to real numbers, if `f` is adapted to `𝒢`, all functions in the sequence `f` are integrable with respect to `μ`, and the conditional expectation of the difference between successive functions in the sequence `f` with respect to the measure `μ` is almost everywhere nonnegative, then `f` is a submartingale with respect to `𝒢` and `μ`.
In simpler terms, the theorem asserts that if we have a sequence of functions that satisfies certain measure-theoretical properties (being adapted to a filtration, being integrable, and having non-negative differences in conditional expectations), then this sequence forms a submartingale, a type of stochastic process with specific "fair game" properties.
More concisely: Given a measurable space `(Ω, m0)`, a filtration `𝒢` over natural numbers, a measure `μ`, and a sequence of `μ`-integrable, `𝒢`-adapted functions `f : ℕ → Ω → ℝ`, if the difference `f (n+1) (x) - f (n) (x)` is almost everywhere nonnegative in the conditional expectation with respect to `μ` for all `n : ℕ` and `x : Ω`, then `f` is a submartingale with respect to `𝒢` and `μ`.
|
MeasureTheory.Martingale.integrable
theorem MeasureTheory.Martingale.integrable :
∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : ι → Ω → E} {ℱ : MeasureTheory.Filtration ι m0},
MeasureTheory.Martingale f ℱ μ → ∀ (i : ι), MeasureTheory.Integrable (f i) μ
The theorem `MeasureTheory.Martingale.integrable` states that for any given preorder ι, measurable space Ω, measure μ on Ω, normed addition commutative group E over real numbers, and a complete normed space E, if there exists a function `f` from ι to Ω to E and a filtration `ℱ` on ι such that `f` is a martingale with respect to `ℱ` and μ, then the function `f` at any index `i` from ι is integrable with respect to μ. In other words, `f` at `i` is measurable and the integral of the norm of `f` at `i` with respect to μ is finite.
More concisely: If `f` is a martingale with respect to filtration `ℱ` and measure `μ` on measurable space `(Ω, Σ)` over complete normed space `E` over real numbers, then each `f(i)` is integrable with respect to `μ`, i.e., both measurable and the integral of the norm of `f(i)` is finite.
|
MeasureTheory.Submartingale.neg
theorem MeasureTheory.Submartingale.neg :
∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : ι → Ω → E} {ℱ : MeasureTheory.Filtration ι m0} [inst_4 : Preorder E]
[inst_5 : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Supermartingale (-f) ℱ μ
This theorem states that for any submartingale `f` with respect to a filtration `ℱ` and a measure `μ`, the negation of `f` (`-f`) is a supermartingale with respect to the same filtration and measure. This is applicable in a measurable space `Ω` with elements of type `E`, where `E` is a complete real normed space. The index type `ι` is assumed to have a preorder relation. This theorem shows the relationship between submartingales and supermartingales under negation in measure theory.
More concisely: For any submartingale `f` in a complete real normed space `Ω` with respect to a filtration `ℱ` and a measure `μ`, the negation `-f` is a supermartingale with respect to the same filtration and measure.
|
MeasureTheory.Submartingale.set_integral_le
theorem MeasureTheory.Submartingale.set_integral_le :
∀ {Ω : Type u_1} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0} [inst_1 : MeasureTheory.SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ},
MeasureTheory.Submartingale f ℱ μ →
∀ {i j : ι}, i ≤ j → ∀ {s : Set Ω}, MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
The theorem `MeasureTheory.Submartingale.set_integral_le` is a fundamental result in Measure Theory. It states that for any types `Ω` and `ι`, given a preorder on `ι`, a measurable space `Ω`, a measure `μ` on `Ω`, a filtration `ℱ` on `Ω`, and a function `f` from `ι` to `Ω` to real numbers that forms a submartingale with respect to `ℱ` and `μ`, then for any two indices `i` and `j` from `ι` with `i` less than or equal to `j`, and for any measurable set `s` of `Ω`, the integral over `s` of the function `f` at index `i` is less than or equal to the integral over `s` of the function `f` at index `j`. In simpler terms, the expected value of a submartingale does not decrease over time, when considering any measurable subset of its domain.
More concisely: For any submartingale `f` over a measurable space `(Ω, ℱ, μ)` with respect to a filtration `ℱ`, the integral of `f(i)` over any measurable set `s` satisfies ∫(si) (fi) dμ ≤ ∫(si) (fj) dμ for all i ≤ j in the index set.
|
MeasureTheory.Martingale.adapted
theorem MeasureTheory.Martingale.adapted :
∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : ι → Ω → E} {ℱ : MeasureTheory.Filtration ι m0},
MeasureTheory.Martingale f ℱ μ → MeasureTheory.Adapted ℱ f
The theorem `MeasureTheory.Martingale.adapted` states that for any given space `Ω` and `E`, any type `ι` with a preorder relation, a measurable space `m0` on `Ω`, a measure `μ` on `Ω`, a sequence of functions `f` from `ι` to `Ω → E`, and a filtration `ℱ` on `m0`, if `f` is a martingale with respect to `ℱ` and the measure `μ`, then `f` is adapted to the filtration `ℱ`. Here, a function sequence is said to be adapted to a filtration if it is strongly measurable for all `ι`. Also, `E` is assumed to be a normed addition commutative group, a normed space over reals, and a complete space.
More concisely: If `f` is a martingale with respect to filtration `ℱ` and measure `μ` on space `Ω` with values in complete, normed real space `E`, then `f` is an adapted sequence.
|