MeasureTheory.Martingale.stoppedValue_min_ae_eq_condexp
theorem MeasureTheory.Martingale.stoppedValue_min_ae_eq_condexp :
∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι]
[inst_4 : LocallyFiniteOrder ι] [inst_5 : OrderBot ι] [inst_6 : TopologicalSpace ι] [inst_7 : DiscreteTopology ι]
[inst_8 : MeasurableSpace ι] [inst_9 : BorelSpace ι] [inst_10 : MeasurableSpace E] [inst_11 : BorelSpace E]
[inst_12 : SecondCountableTopology E] {ℱ : MeasureTheory.Filtration ι m} {τ σ : Ω → ι} {f : ι → Ω → E}
[inst_13 : MeasureTheory.SigmaFiniteFiltration μ ℱ],
MeasureTheory.Martingale f ℱ μ →
∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) (hσ : MeasureTheory.IsStoppingTime ℱ σ) {n : ι},
(∀ (x : Ω), τ x ≤ n) →
∀ [h_sf_min : MeasureTheory.SigmaFinite (μ.trim ⋯)],
μ.ae.EventuallyEq (MeasureTheory.stoppedValue f fun x => min (σ x) (τ x))
(MeasureTheory.condexp hσ.measurableSpace μ (MeasureTheory.stoppedValue f τ))
The **Optional Sampling theorem** states that if `τ` is a bounded stopping time and `σ` is another stopping time, then in the context of a martingale `f`, the value of `f` at the stopping time given by the minimum of `τ` and `σ`, is almost everywhere equal to the conditional expectation of `f` stopped at `τ` with respect to the σ-algebra generated by `σ`. This theorem is applicable under the conditions that the measure space and measurable space being worked with satisfy certain properties like being a Borel space, having a second countable topology, etc., and that the stopping times `τ` and `σ` are measurable with respect to a filtration `ℱ`. It further requires that `τ` is bounded by some `n`, i.e., for every point in the measure space, the value of the stopping time `τ` at that point does not exceed `n`. The theorem is a key result in the theory of martingales, particularly in the context of stopping times and filtrations, providing a relationship between the stopped values and conditional expectations of functions.
More concisely: If `τ` and `σ` are bounded, measurable stopping times in a martingale `f` over a second countable Borel space, then almost everywhere `f`(min(`τ`, `σ`)) = E[`f` | σ]^ℱ, where E[• | σ]^ℱ denotes the conditional expectation with respect to the σ-algebra generated by `σ` under filtration `ℱ`.
|
MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const_of_countable_range
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const_of_countable_range :
∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι]
[inst_4 : TopologicalSpace ι] [inst_5 : OrderTopology ι] [inst_6 : FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m} [inst_7 : MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ : Ω → ι} {f : ι → Ω → E}
{n : ι},
MeasureTheory.Martingale f ℱ μ →
∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ n),
(Set.range τ).Countable →
∀ [inst_8 : MeasureTheory.SigmaFinite (μ.trim ⋯)],
μ.ae.EventuallyEq (MeasureTheory.stoppedValue f τ) (MeasureTheory.condexp hτ.measurableSpace μ (f n))
This theorem states that for a martingale `f` with respect to a filtration `ℱ` on a measurable space `Ω` and a measure `μ`, given a stopping time `τ` which is bounded by a constant `n`, the value of the martingale at the stopping time is equal to the conditional expectation of `f` at time `n` with respect to the σ-algebra generated by `τ`. This is true under the conditions that the range of `τ` is countable and the measure `μ` is σ-finite with respect to the trimmed filtration. The term "martingale" refers to a sequence of random variables where the expectation of the next step is equal to the current value, and "stopping time" is a specific time at which a certain condition is met. The conditional expectation is the expected value of a random variable given information up to a certain time.
More concisely: For a countable-valued martingale `f` on a σ-finite measure space `(Ω, ℱ, μ)` with respect to a filtration `ℱ`, if `τ` is a bounded stopping time, then `f(τ) = ℙ[τ <= n | ℱ(n)] * E[f(n) | ℱ(n)]`, where `n` is a natural number and `E` denotes the conditional expectation with respect to `ℱ`.
|
MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const :
∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι]
[inst_4 : TopologicalSpace ι] [inst_5 : OrderTopology ι] [inst_6 : FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m} [inst_7 : MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ : Ω → ι} {f : ι → Ω → E}
{n : ι} [inst_8 : Countable ι],
MeasureTheory.Martingale f ℱ μ →
∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ n)
[inst_9 : MeasureTheory.SigmaFinite (μ.trim ⋯)],
μ.ae.EventuallyEq (MeasureTheory.stoppedValue f τ) (MeasureTheory.condexp hτ.measurableSpace μ (f n))
The theorem states that for a martingale `f`, given a stopping time `τ` that is bounded by a constant `n`, the "stopped value" of `f` at `τ` is equal to the conditional expectation of `f` at time `n` with respect to the σ-algebra generated by `τ`.
In other words, the martingale's value at the stopping time is on average the same as the expected value of the martingale at a fixed later time `n`, when conditioned on the events known at the stopping time. This holds almost everywhere with respect to a given probability measure `μ`.
This theorem is a significant result in stochastic calculus and financial mathematics, providing insight into the behavior of martingales and their stopped processes.
More concisely: For a martingale `f` and a bounded stopping time `τ`, the stopped value `f`(τ) equals the conditional expectation of `f`(n) given the σ-algebra generated by `τ`, almost everywhere with respect to a probability measure `μ`.
|
MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_of_countable_range
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_of_countable_range :
∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι]
[inst_4 : TopologicalSpace ι] [inst_5 : OrderTopology ι] [inst_6 : FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m} [inst_7 : MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ σ : Ω → ι}
{f : ι → Ω → E} {n : ι},
MeasureTheory.Martingale f ℱ μ →
MeasureTheory.IsStoppingTime ℱ τ →
∀ (hσ : MeasureTheory.IsStoppingTime ℱ σ) (hσ_le_τ : σ ≤ τ) (hτ_le : ∀ (x : Ω), τ x ≤ n),
(Set.range τ).Countable →
(Set.range σ).Countable →
∀ [inst_8 : MeasureTheory.SigmaFinite (μ.trim ⋯)],
μ.ae.EventuallyEq (MeasureTheory.stoppedValue f σ)
(MeasureTheory.condexp hσ.measurableSpace μ (MeasureTheory.stoppedValue f τ))
The theorem states that if `τ` and `σ` are two stopping times such that `σ` is less than or equal to `τ` and `τ` is bounded, then the value of a martingale `f` at `σ` is the conditional expectation of its value at `τ` with respect to the σ-algebra generated by `σ`. This is under the condition that the set of values taken by `τ` and `σ` are countable and `f` is a martingale with respect to the filtration `ℱ` and the measure `μ`. A stopping time here refers to a rule that determines when to stop a process based on the state of the process at the current time. The value of the martingale `f` at a stopping time is obtained by applying the function `f` at the time indicated by the stopping time. The conditional expectation is the expected value of a random variable given the outcome of another random variable.
More concisely: If `τ` and `σ` are countable, bounded stopping times with `σ ≤ τ` for a countable filtration `ℱ` and measure `μ`, and `f` is a `ℱ`-martingale, then `ℰ[f(τ) | ℱσ] = f(σ)` almost surely.
|
MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le :
∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι]
[inst_4 : TopologicalSpace ι] [inst_5 : OrderTopology ι] [inst_6 : FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m} [inst_7 : MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ σ : Ω → ι}
{f : ι → Ω → E} {n : ι} [inst_8 : Countable ι],
MeasureTheory.Martingale f ℱ μ →
MeasureTheory.IsStoppingTime ℱ τ →
∀ (hσ : MeasureTheory.IsStoppingTime ℱ σ),
σ ≤ τ →
(∀ (x : Ω), τ x ≤ n) →
∀ [inst_9 : MeasureTheory.SigmaFinite (μ.trim ⋯)],
μ.ae.EventuallyEq (MeasureTheory.stoppedValue f σ)
(MeasureTheory.condexp hσ.measurableSpace μ (MeasureTheory.stoppedValue f τ))
The theorem `MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le` states the following: Given a martingale `f` and two stopping times `σ` and `τ` such that `σ` is less than or equal to `τ` and `τ` is bounded, the value of the martingale `f` at the stopping time `σ` is almost-everywhere equal to the conditional expectation of its value at the stopping time `τ`. This is with respect to the σ-algebra generated by the stopping time `σ`. In other words, if we stop the martingale `f` at time `σ`, its value is essentially the expected future value if we had instead stopped it later at time `τ`, given what we know at time `σ`.
More concisely: For a bounded martingale $f$ and stopping times $\sigma$ and $\tau$ with $\sigma \leq \tau$, almost-everywhere $\sigma$-measurable, $f(\sigma) = \operatorname{E}[f(\tau) \mid \sigma]$.
|