theorem
MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le_of_countable_range
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace.MetrizableSpace ι]
{mΩ : MeasurableSpace Ω}
{𝓕 : Filtration ι mΩ}
{μ : Measure Ω}
[IsFiniteMeasure μ]
{X : ι → Ω → ℝ}
{τ σ : Ω → WithTop ι}
(h : Martingale X 𝓕 μ)
(hRC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
{i : ι}
(hτ_le : ∀ (x : Ω), τ x ≤ ↑i)
(hτ : IsStoppingTime 𝓕 τ)
(hσ : IsStoppingTime 𝓕 σ)
(hτ_countable_range : (Set.range τ).Countable)
:
theorem
MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp_of_countable_range
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace.MetrizableSpace ι]
{mΩ : MeasurableSpace Ω}
{𝓕 : Filtration ι mΩ}
{μ : Measure Ω}
[IsFiniteMeasure μ]
{X : ι → Ω → ℝ}
{τ σ : Ω → WithTop ι}
(h : Martingale X 𝓕 μ)
(hRC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
(hτ : IsStoppingTime 𝓕 τ)
(hσ : IsStoppingTime 𝓕 σ)
{n : ι}
(hτ_le : ∀ (x : Ω), τ x ≤ ↑n)
(hτ_countable_range : (Set.range τ).Countable)
(hσ_countable_range : (Set.range σ).Countable)
:
theorem
MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp_of_discreteApproxSequence
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace.MetrizableSpace ι]
{mΩ : MeasurableSpace Ω}
{𝓕 : Filtration ι mΩ}
{μ : Measure Ω}
[IsFiniteMeasure μ]
{X : ι → Ω → ℝ}
{τ σ : Ω → WithTop ι}
(h : Martingale X 𝓕 μ)
(hRC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
(hτ : IsStoppingTime 𝓕 τ)
(hσ : IsStoppingTime 𝓕 σ)
{n : ι}
(hτ_le : ∀ (x : Ω), τ x ≤ ↑n)
(τn : DiscreteApproxSequence 𝓕 τ μ)
(σn : DiscreteApproxSequence 𝓕 σ μ)
:
Optional sampling theorem for general time indices
(assuming existence of DiscreteApproxSequence).
theorem
MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp'
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace.MetrizableSpace ι]
{mΩ : MeasurableSpace Ω}
{𝓕 : Filtration ι mΩ}
{μ : Measure Ω}
[IsFiniteMeasure μ]
{X : ι → Ω → ℝ}
{τ σ : Ω → WithTop ι}
[Approximable 𝓕 μ]
(h : Martingale X 𝓕 μ)
(hRC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
(hτ : IsStoppingTime 𝓕 τ)
(hσ : IsStoppingTime 𝓕 σ)
{n : ι}
(hτ_le : ∀ (x : Ω), τ x ≤ ↑n)
:
Optional sampling theorem for approximable time indices.
theorem
MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_discreteApproxSequence
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace.MetrizableSpace ι]
{mΩ : MeasurableSpace Ω}
{𝓕 : Filtration ι mΩ}
{μ : Measure Ω}
[IsFiniteMeasure μ]
{X : ι → Ω → ℝ}
{τ : Ω → WithTop ι}
{n : ι}
[Approximable 𝓕 μ]
(h : Martingale X 𝓕 μ)
(hRC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
(hτ : IsStoppingTime 𝓕 τ)
(hτ_le : ∀ (x : Ω), τ x ≤ ↑n)
:
theorem
MeasureTheory.Submartingale.stoppedValue_min_ae_le_condExp_nat
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{σ τ : Ω → WithTop ℕ}
{X : ℕ → Ω → E}
(𝓕 : Filtration ℕ mΩ)
[PartialOrder E]
[OrderClosedTopology E]
[IsOrderedModule ℝ E]
[IsOrderedAddMonoid E]
(hX : Submartingale X 𝓕 P)
{k : ℕ}
(hτk : ∀ᵐ (ω : Ω) ∂P, τ ω ≤ ↑k)
(hσ : IsStoppingTime 𝓕 σ)
(hτ : IsStoppingTime 𝓕 τ)
:
theorem
MeasureTheory.Supermartingale.condExp_ae_le_stoppedValue_min_nat
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{σ τ : Ω → WithTop ℕ}
{X : ℕ → Ω → E}
(𝓕 : Filtration ℕ mΩ)
[PartialOrder E]
[OrderClosedTopology E]
[IsOrderedModule ℝ E]
[IsOrderedAddMonoid E]
(hX : Supermartingale X 𝓕 P)
{k : ℕ}
(hτk : ∀ᵐ (ω : Ω) ∂P, τ ω ≤ ↑k)
(hσ : IsStoppingTime 𝓕 σ)
(hτ : IsStoppingTime 𝓕 τ)
:
theorem
MeasureTheory.Submartingale.stoppedValue_min_ae_le_condExp
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace.MetrizableSpace ι]
{σ τ : Ω → WithTop ι}
{X : ι → Ω → E}
(𝓕 : Filtration ι mΩ)
[PartialOrder E]
[OrderClosedTopology E]
[IsOrderedModule ℝ E]
[IsOrderedAddMonoid E]
(hX1 : Submartingale X 𝓕 P)
(hX2 : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
{k : ι}
(hτk : ∀ᵐ (ω : Ω) ∂P, τ ω ≤ ↑k)
(hσ : IsStoppingTime 𝓕 σ)
(hτ : IsStoppingTime 𝓕 τ)
: