Limit of a stochastic process #
Under certain assumptions, classical familes of processes such as martingales converge as time
goes to infinity, and several important properties of the process can be inferred from this limit,
so that it is useful to be able to refer to this limit via a definition.
This file thus provides a definition 𝓕.limitProcess X P, which is the limit of the process X
under the measure P with an ambient filtration 𝓕. This is defined for any X : ι → Ω → E,
but of course it only makes sense if X converges. Moreover, in concrete use cases, X will
be strongly adapted to the filtration 𝓕, so that the limit will be ⨆ t, 𝓕 t-strongly measurable.
Therefore we define 𝓕.limitProcess X P to be a ⨆ t, 𝓕 t-strongly measurable almost everywhere
limit if it exists, and 0 otherwise.
This definition is for example used to phrase the a.e. martingale convergence theorem
Submartingale.ae_tendsto_limitProcess where an L¹-bounded submartingale X adapted to 𝓕
converges to limitProcess X 𝓕 P P-almost everywhere.
In this file we provide the definition and prove basic preservation properties of the limit under continuous maps.
Because several properties often rely on the fact that the limit exists, we also define a predicate
HasLimitProcess X 𝓕 P which states that X does converge P-almost surely towards a
⨆ t, 𝓕 t-strongly measurable function.
HasLimitProcess predicate #
def
MeasureTheory.Filtration.HasLimitProcess
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
(X : ι → Ω → E)
(𝓕 : Filtration ι mΩ)
(P : Measure Ω)
:
A stochastic process X satisfies 𝓕.HasLimitProcess X P if it converges P-almost surely
towards a ⨆ t, 𝓕 t-strongly measurable random variable.
Equations
- MeasureTheory.Filtration.HasLimitProcess X 𝓕 P = ∃ (g : Ω → E), MeasureTheory.StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ι) => X x ω) Filter.atTop (nhds (g ω))
Instances For
theorem
MeasureTheory.Filtration.HasLimitProcess.congr
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
(h : X ≡ᵐ[P] Y)
(hX : HasLimitProcess X 𝓕 P)
:
HasLimitProcess Y 𝓕 P
theorem
MeasureTheory.Filtration.hasLimitProcess_congr_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
(h : X ≡ᵐ[P] Y)
:
theorem
MeasureTheory.Filtration.HasLimitProcess.comp
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{F : Type u_4}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
[TopologicalSpace F]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{f : E → F}
(hX : HasLimitProcess X 𝓕 P)
(hf : Continuous f)
:
HasLimitProcess (fun (t : ι) (ω : Ω) => f (X t ω)) 𝓕 P
theorem
MeasureTheory.Filtration.HasLimitProcess.comp₂
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
[TopologicalSpace F]
[TopologicalSpace G]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{Z : ι → Ω → F}
{f : E → F → G}
(hX : HasLimitProcess X 𝓕 P)
(hZ : HasLimitProcess Z 𝓕 P)
(hf : Continuous (Function.uncurry f))
:
HasLimitProcess (fun (t : ι) (ω : Ω) => f (X t ω) (Z t ω)) 𝓕 P
theorem
MeasureTheory.Filtration.HasLimitProcess.smul
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{G : Type u_6}
[SMul G E]
[ContinuousConstSMul G E]
(c : G)
(hX : HasLimitProcess X 𝓕 P)
:
HasLimitProcess (c • X) 𝓕 P
theorem
MeasureTheory.Filtration.HasLimitProcess.vadd
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{G : Type u_6}
[VAdd G E]
[ContinuousConstVAdd G E]
(c : G)
(hX : HasLimitProcess X 𝓕 P)
:
HasLimitProcess (c +ᵥ X) 𝓕 P
theorem
MeasureTheory.Filtration.hasLimitProcess_smul_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{G : Type u_6}
[Group G]
[MulAction G E]
[ContinuousConstSMul G E]
{c : G}
:
theorem
MeasureTheory.Filtration.hasLimitProcess_vadd_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{G : Type u_6}
[AddGroup G]
[AddAction G E]
[ContinuousConstVAdd G E]
{c : G}
:
theorem
MeasureTheory.Filtration.HasLimitProcess.of_smul
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{G : Type u_6}
[Group G]
[MulAction G E]
[ContinuousConstSMul G E]
{c : G}
:
HasLimitProcess (c • X) 𝓕 P → HasLimitProcess X 𝓕 P
Alias of the forward direction of MeasureTheory.Filtration.hasLimitProcess_smul_iff.
theorem
MeasureTheory.Filtration.HasLimitProcess.of_vadd
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{G : Type u_6}
[AddGroup G]
[AddAction G E]
[ContinuousConstVAdd G E]
{c : G}
:
HasLimitProcess (c +ᵥ X) 𝓕 P → HasLimitProcess X 𝓕 P
Alias of the forward direction of MeasureTheory.Filtration.hasLimitProcess_vadd_iff.
theorem
MeasureTheory.Filtration.hasLimitProcess_smul_iff₀
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{G : Type u_6}
[GroupWithZero G]
[MulAction G E]
[ContinuousConstSMul G E]
{c : G}
(hc : c ≠ 0)
:
theorem
MeasureTheory.Filtration.HasLimitProcess.of_smul₀
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{G : Type u_6}
[GroupWithZero G]
[MulAction G E]
[ContinuousConstSMul G E]
{c : G}
(hc : c ≠ 0)
:
HasLimitProcess (c • X) 𝓕 P → HasLimitProcess X 𝓕 P
Alias of the forward direction of MeasureTheory.Filtration.hasLimitProcess_smul_iff₀.
theorem
MeasureTheory.Filtration.HasLimitProcess.inv
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[Inv E]
[ContinuousInv E]
(hX : HasLimitProcess X 𝓕 P)
:
HasLimitProcess X⁻¹ 𝓕 P
theorem
MeasureTheory.Filtration.HasLimitProcess.neg
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[Neg E]
[ContinuousNeg E]
(hX : HasLimitProcess X 𝓕 P)
:
HasLimitProcess (-X) 𝓕 P
theorem
MeasureTheory.Filtration.hasLimitProcess_inv_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[InvolutiveInv E]
[ContinuousInv E]
:
theorem
MeasureTheory.Filtration.hasLimitProcess_neg_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[InvolutiveNeg E]
[ContinuousNeg E]
:
theorem
MeasureTheory.Filtration.HasLimitProcess.of_inv
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[InvolutiveInv E]
[ContinuousInv E]
:
HasLimitProcess X⁻¹ 𝓕 P → HasLimitProcess X 𝓕 P
Alias of the forward direction of MeasureTheory.Filtration.hasLimitProcess_inv_iff.
theorem
MeasureTheory.Filtration.HasLimitProcess.of_neg
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[InvolutiveNeg E]
[ContinuousNeg E]
:
HasLimitProcess (-X) 𝓕 P → HasLimitProcess X 𝓕 P
Alias of the forward direction of MeasureTheory.Filtration.hasLimitProcess_neg_iff.
theorem
MeasureTheory.Filtration.HasLimitProcess.mul
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[Mul E]
[ContinuousMul E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
HasLimitProcess (X * Y) 𝓕 P
theorem
MeasureTheory.Filtration.HasLimitProcess.add
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[Add E]
[ContinuousAdd E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
HasLimitProcess (X + Y) 𝓕 P
theorem
MeasureTheory.Filtration.HasLimitProcess.div'
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[Div E]
[ContinuousDiv E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
HasLimitProcess (X / Y) 𝓕 P
theorem
MeasureTheory.Filtration.HasLimitProcess.sub
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[Sub E]
[ContinuousSub E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
HasLimitProcess (X - Y) 𝓕 P
theorem
MeasureTheory.Filtration.HasLimitProcess.prodMk
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{F : Type u_4}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
[TopologicalSpace F]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{Z : ι → Ω → F}
(hX : HasLimitProcess X 𝓕 P)
(hZ : HasLimitProcess Z 𝓕 P)
:
HasLimitProcess (fun (t : ι) (ω : Ω) => (X t ω, Z t ω)) 𝓕 P
The limit of a process #
noncomputable def
MeasureTheory.Filtration.limitProcess
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
[Zero E]
(X : ι → Ω → E)
(𝓕 : Filtration ι mΩ)
(P : Measure Ω)
:
Ω → E
Given a process X and a filtration 𝓕, if X converges to some g almost everywhere and
g is ⨆ t, 𝓕 t-measurable (i.e. HasLimitProcess X 𝓕 P holds),
then limitProcess X 𝓕 P chooses said g, else it returns 0.
This definition is used to phrase the a.e. martingale convergence theorem
Submartingale.ae_tendsto_limitProcess where an L¹-bounded submartingale X adapted to 𝓕
converges to limitProcess X 𝓕 P P-almost everywhere.
Equations
- MeasureTheory.Filtration.limitProcess X 𝓕 P = if h : MeasureTheory.Filtration.HasLimitProcess X 𝓕 P then Exists.choose h else 0
Instances For
theorem
MeasureTheory.Filtration.HasLimitProcess.ae_tendsto_limitProcess
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[Zero E]
(h : HasLimitProcess X 𝓕 P)
:
∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ι) => X x ω) Filter.atTop (nhds (limitProcess X 𝓕 P ω))
theorem
MeasureTheory.Filtration.stronglyMeasurable_limitProcess
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[Zero E]
:
StronglyMeasurable (limitProcess X 𝓕 P)
theorem
MeasureTheory.Filtration.stronglyMeasurable_limit_process'
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[Zero E]
:
StronglyMeasurable (limitProcess X 𝓕 P)
theorem
MeasureTheory.Filtration.limitProcess_ae_eq
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
{g : Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
(mg : StronglyMeasurable g)
(hg : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ι) => X x ω) Filter.atTop (nhds (g ω)))
:
limitProcess X 𝓕 P =ᵐ[P] g
If X converges almost surely towards g a ⨆ t, 𝓕 t-strongly measurable function,
then g is almost surely equal to 𝓕.limitProcess X P.
theorem
MeasureTheory.Filtration.limitProcess_congr
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[IsDirectedOrder ι]
[T2Space E]
[Zero E]
(hXY : X ≡ᵐ[P] Y)
:
limitProcess X 𝓕 P =ᵐ[P] limitProcess Y 𝓕 P
theorem
MeasureTheory.Filtration.limitProcess_const
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
(c : E)
:
limitProcess (fun (x : ι) (x_1 : Ω) => c) 𝓕 P =ᵐ[P] fun (x : Ω) => c
theorem
MeasureTheory.Filtration.limitProcess_zero
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
:
limitProcess 0 𝓕 P =ᵐ[P] 0
theorem
MeasureTheory.Filtration.HasLimitProcess.limitProcess_comp
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
{F : Type u_6}
[Zero F]
[TopologicalSpace F]
[Zero E]
[T2Space F]
{f : E → F}
(hf : Continuous f)
(hX : HasLimitProcess X 𝓕 P)
:
limitProcess (fun (t : ι) (ω : Ω) => f (X t ω)) 𝓕 P =ᵐ[P] f ∘ limitProcess X 𝓕 P
theorem
MeasureTheory.Filtration.HasLimitProcess.limitProcess_fun_comp
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
{F : Type u_6}
[Zero F]
[TopologicalSpace F]
[Zero E]
[T2Space F]
{f : E → F}
(hf : Continuous f)
(hX : HasLimitProcess X 𝓕 P)
:
limitProcess (fun (t : ι) (ω : Ω) => f (X t ω)) 𝓕 P =ᵐ[P] fun (x : Ω) => f (limitProcess X 𝓕 P x)
Eta-expanded form of MeasureTheory.Filtration.HasLimitProcess.limitProcess_comp
theorem
MeasureTheory.Filtration.HasLimitProcess.limitProcess_comp₂
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
{F : Type u_6}
{G : Type u_7}
[Zero F]
[TopologicalSpace F]
[Zero G]
[TopologicalSpace G]
[Zero E]
[T2Space G]
{f : E → F → G}
(hf : Continuous (Function.uncurry f))
{Y : ι → Ω → F}
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
limitProcess (fun (t : ι) (ω : Ω) => f (X t ω) (Y t ω)) 𝓕 P =ᵐ[P] fun (ω : Ω) =>
f (limitProcess X 𝓕 P ω) (limitProcess Y 𝓕 P ω)
theorem
MeasureTheory.Filtration.HasLimitProcess.limitProcess_vadd
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
{G : Type u_8}
[VAdd G E]
[ContinuousConstVAdd G E]
(c : G)
(hX : HasLimitProcess X 𝓕 P)
:
limitProcess (c +ᵥ X) 𝓕 P =ᵐ[P] c +ᵥ limitProcess X 𝓕 P
theorem
MeasureTheory.Filtration.HasLimitProcess.limitProcess_fun_vadd
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
{G : Type u_8}
[VAdd G E]
[ContinuousConstVAdd G E]
(c : G)
(hX : HasLimitProcess X 𝓕 P)
:
limitProcess (fun (i : ι) (i_1 : Ω) => c +ᵥ X i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) => c +ᵥ limitProcess X 𝓕 P i
Eta-expanded form of MeasureTheory.Filtration.HasLimitProcess.limitProcess_vadd
theorem
MeasureTheory.Filtration.limitProcess_smul
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
{G : Type u_8}
[GroupWithZero G]
[MulActionWithZero G E]
[ContinuousConstSMul G E]
(X : ι → Ω → E)
(c : G)
:
limitProcess (c • X) 𝓕 P =ᵐ[P] c • limitProcess X 𝓕 P
theorem
MeasureTheory.Filtration.limitProcess_fun_smul
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
{G : Type u_8}
[GroupWithZero G]
[MulActionWithZero G E]
[ContinuousConstSMul G E]
(X : ι → Ω → E)
(c : G)
:
limitProcess (fun (i : ι) (i_1 : Ω) => c • X i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) => c • limitProcess X 𝓕 P i
Eta-expanded form of MeasureTheory.Filtration.limitProcess_smul
theorem
MeasureTheory.Filtration.limitProcess_neg
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[AddGroup E]
[ContinuousNeg E]
(X : ι → Ω → E)
:
limitProcess (-X) 𝓕 P =ᵐ[P] -limitProcess X 𝓕 P
theorem
MeasureTheory.Filtration.limitProcess_fun_neg
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[AddGroup E]
[ContinuousNeg E]
(X : ι → Ω → E)
:
limitProcess (fun (i : ι) (i_1 : Ω) => -X i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) => -limitProcess X 𝓕 P i
Eta-expanded form of MeasureTheory.Filtration.limitProcess_neg
theorem
MeasureTheory.Filtration.limitProcess_mul
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
[Mul E]
[ContinuousMul E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
limitProcess (X * Y) 𝓕 P =ᵐ[P] limitProcess X 𝓕 P * limitProcess Y 𝓕 P
theorem
MeasureTheory.Filtration.limitProcess_fun_mul
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
[Mul E]
[ContinuousMul E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
limitProcess (fun (i : ι) (i_1 : Ω) => X i i_1 * Y i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) =>
limitProcess X 𝓕 P i * limitProcess Y 𝓕 P i
Eta-expanded form of MeasureTheory.Filtration.limitProcess_mul
theorem
MeasureTheory.Filtration.limitProcess_fun_add
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
[Add E]
[ContinuousAdd E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
limitProcess (fun (i : ι) (i_1 : Ω) => X i i_1 + Y i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) =>
limitProcess X 𝓕 P i + limitProcess Y 𝓕 P i
theorem
MeasureTheory.Filtration.limitProcess_add
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
[Add E]
[ContinuousAdd E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
limitProcess (X + Y) 𝓕 P =ᵐ[P] limitProcess X 𝓕 P + limitProcess Y 𝓕 P
theorem
MeasureTheory.Filtration.limitProcess_div'
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
[Div E]
[ContinuousDiv E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
limitProcess (X / Y) 𝓕 P =ᵐ[P] limitProcess X 𝓕 P / limitProcess Y 𝓕 P
theorem
MeasureTheory.Filtration.limitProcess_fun_div'
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
[Div E]
[ContinuousDiv E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
limitProcess (fun (i : ι) (i_1 : Ω) => X i i_1 / Y i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) =>
limitProcess X 𝓕 P i / limitProcess Y 𝓕 P i
Eta-expanded form of MeasureTheory.Filtration.limitProcess_div'
theorem
MeasureTheory.Filtration.limitProcess_sub
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
[Sub E]
[ContinuousSub E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
limitProcess (X - Y) 𝓕 P =ᵐ[P] limitProcess X 𝓕 P - limitProcess Y 𝓕 P
theorem
MeasureTheory.Filtration.limitProcess_fun_sub
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
[Sub E]
[ContinuousSub E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
limitProcess (fun (i : ι) (i_1 : Ω) => X i i_1 - Y i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) =>
limitProcess X 𝓕 P i - limitProcess Y 𝓕 P i
theorem
MeasureTheory.Filtration.limitProcess_prodMk
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[Preorder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace E]
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{X Y : ι → Ω → E}
[IsDirectedOrder ι]
[Nonempty ι]
[T2Space E]
[Zero E]
(hX : HasLimitProcess X 𝓕 P)
(hY : HasLimitProcess Y 𝓕 P)
:
limitProcess (fun (t : ι) (ω : Ω) => (X t ω, Y t ω)) 𝓕 P =ᵐ[P] fun (ω : Ω) =>
(limitProcess X 𝓕 P ω, limitProcess Y 𝓕 P ω)
theorem
MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{R : NNReal}
{p : ENNReal}
{F : Type u_6}
[SeminormedAddGroup F]
{𝓕 : Filtration ℕ mΩ}
{X : ℕ → Ω → F}
(hfm : ∀ (n : ℕ), AEStronglyMeasurable (X n) P)
(hbdd : ∀ (n : ℕ), eLpNorm (X n) p P ≤ ↑R)
:
MemLp (limitProcess X 𝓕 P) p P
If a stochastic process is bounded in Lp then its limit is in Lp.