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.smul
{ι : 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)
(r : ℝ)
:
IsSquareIntegrable (fun (i : ι) (ω : Ω) => r • X 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.SigmaFiniteFiltration 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.SigmaFiniteFiltration P 𝓕]
(hX : IsSquareIntegrable X 𝓕 P)
{i j : ι}
(hij : i ≤ j)
:
theorem
ProbabilityTheory.IsSquareIntegrable.ae_tendsto_limitProcess
{ι : 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.SigmaFiniteFiltration P 𝓕]
(hX : IsSquareIntegrable X 𝓕 P)
:
∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ι) => X x ω) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess X 𝓕 P ω))
theorem
ProbabilityTheory.IsSquareIntegrable.tendsto_eLpNorm_two_limitProcess
{ι : 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.SigmaFiniteFiltration P 𝓕]
(hX : IsSquareIntegrable X 𝓕 P)
:
Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (X i - MeasureTheory.Filtration.limitProcess X 𝓕 P) 2 P)
Filter.atTop (nhds 0)