Properties of martingales and submartingales #
theorem
MeasureTheory.Martingale.congr
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X Y : ι → Ω → E}
{𝓕 : Filtration ι mΩ}
(hX : Martingale X 𝓕 P)
(hY : Adapted 𝓕 Y)
(h_eq : ∀ (t : ι), X t =ᶠ[ae P] Y t)
:
Martingale Y 𝓕 P
theorem
MeasureTheory.Submartingale.congr
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X Y : ι → Ω → E}
{𝓕 : Filtration ι mΩ}
[LE E]
(hX : Submartingale X 𝓕 P)
(hY : Adapted 𝓕 Y)
(h_eq : ∀ (t : ι), X t =ᶠ[ae P] Y t)
:
Submartingale Y 𝓕 P
theorem
MeasureTheory.Martingale.submartingale_convex_comp
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
[SigmaFinite P]
{X : ι → Ω → E}
{𝓕 : Filtration ι mΩ}
(hX : Martingale X 𝓕 P)
{φ : E → ℝ}
(hφ_cvx : ConvexOn ℝ Set.univ φ)
(hφ_cont : Continuous φ)
(hφ_int : ∀ (t : ι), Integrable (fun (ω : Ω) => φ (X t ω)) P)
:
Submartingale (fun (t : ι) (ω : Ω) => φ (X t ω)) 𝓕 P
theorem
MeasureTheory.Martingale.submartingale_norm
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
[SigmaFinite P]
{X : ι → Ω → E}
{𝓕 : Filtration ι mΩ}
(hX : Martingale X 𝓕 P)
:
Submartingale (fun (t : ι) (ω : Ω) => ‖X t ω‖) 𝓕 P
theorem
MeasureTheory.Submartingale.monotone_convex_comp
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
[SigmaFinite P]
{X : ι → Ω → E}
{𝓕 : Filtration ι mΩ}
[Preorder E]
(hX : Submartingale X 𝓕 P)
{φ : E → ℝ}
(hφ_mono : Monotone φ)
(hφ_cvx : ConvexOn ℝ Set.univ φ)
(hφ_cont : Continuous φ)
(hφ_int : ∀ (t : ι), Integrable (fun (ω : Ω) => φ (X t ω)) P)
:
Submartingale (fun (t : ι) (ω : Ω) => φ (X t ω)) 𝓕 P