Square integrable martingales #
structure
ProbabilityTheory.IsSquareIntegrable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ 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
def
ProbabilityTheory.IsLocallySquareIntegrable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{mΩ : MeasurableSpace Ω}
[OrderBot ι]
[OrderTopology ι]
(X : ι → Ω → E)
(𝓕 : MeasureTheory.Filtration ι mΩ)
(P : MeasureTheory.Measure Ω := by volume_tac)
:
A stochastic process is locally square-integrable if it satisfies the square-integrable martingale property locally.
Equations
- ProbabilityTheory.IsLocallySquareIntegrable X 𝓕 P = ProbabilityTheory.Locally (fun (Y : ι → Ω → E) => ProbabilityTheory.IsSquareIntegrable Y 𝓕 P) 𝓕 X P
Instances For
theorem
ProbabilityTheory.IsSquareIntegrable.isLocallySquareIntegrable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
[OrderTopology ι]
(hX : IsSquareIntegrable X 𝓕 P)
:
theorem
ProbabilityTheory.IsSquareIntegrable.integrable_sq
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ 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]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[CompleteSpace E]
(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]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[CompleteSpace E]
(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]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[MeasureTheory.SigmaFiniteFiltration P 𝓕]
[CompleteSpace E]
(hX : IsSquareIntegrable X 𝓕 P)
:
MeasureTheory.Submartingale (fun (i : ι) (ω : Ω) => ‖X i ω‖ ^ 2) 𝓕 P
theorem
ProbabilityTheory.IsLocallySquareIntegrable.isLocalSubmartingale_sq_norm
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[MeasureTheory.SigmaFiniteFiltration P 𝓕]
[OrderBot ι]
[OrderTopology ι]
[CompleteSpace E]
(hX : IsLocallySquareIntegrable X 𝓕 P)
:
IsLocalSubmartingale (fun (t : ι) (ω : Ω) => ‖X t ω‖ ^ 2) 𝓕 P
A locally square-integrable martingale has locally submartingale squared norm.
theorem
ProbabilityTheory.IsSquareIntegrable.eLpNorm_mono
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[MeasureTheory.SigmaFiniteFiltration P 𝓕]
[CompleteSpace E]
(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]
{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]
{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)