Square integrable martingales #
structure
ProbabilityTheory.IsSquareIntegrable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
(X : ι → Ω → E)
(𝓕 : MeasureTheory.Filtration ι mΩ)
(P : MeasureTheory.Measure Ω)
:
A square integrable martingale is a martingale with cadlag paths and uniformly bounded second moments.
- martingale : MeasureTheory.Martingale X 𝓕 P
- cadlag (ω : Ω) : IsCadlag fun (x : ι) => X x ω
Instances For
theorem
ProbabilityTheory.IsSquareIntegrable.integrable_sq
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : IsSquareIntegrable X 𝓕 P)
(i : ι)
:
MeasureTheory.Integrable (fun (ω : Ω) => ‖X i ω‖ ^ 2) P
theorem
ProbabilityTheory.IsSquareIntegrable.add
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : IsSquareIntegrable X 𝓕 P)
(hY : IsSquareIntegrable Y 𝓕 P)
:
IsSquareIntegrable (fun (i : ι) (ω : Ω) => X i ω + Y i ω) 𝓕 P
theorem
ProbabilityTheory.IsSquareIntegrable.submartingale_sq_norm
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[MeasureTheory.SigmaFinite P]
(hX : IsSquareIntegrable X 𝓕 P)
:
MeasureTheory.Submartingale (fun (i : ι) (ω : Ω) => ‖X i ω‖ ^ 2) 𝓕 P
theorem
ProbabilityTheory.IsSquareIntegrable.eLpNorm_mono
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[MeasureTheory.SigmaFinite P]
[MeasureTheory.SigmaFiniteFiltration P 𝓕]
(hX : IsSquareIntegrable X 𝓕 P)
{i j : ι}
(hij : i ≤ j)
: