Pairing a càdlàg path with a continuous path #
The pair of a càdlàg real path and a continuous real path is a càdlàg path with values in
ℝ × ℝ. The pairing map is jointly continuous for the Skorokhod J1 topology and the uniform
topology on continuous paths. The same time changes control both coordinates; in the continuous
coordinate one also uses uniform convergence and uniform continuity of the limiting path.
Reference: P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Section 12.
def
BGW.Skorokhod.prodWithCont
{T : ℝ}
{E : Type u_1}
{F : Type u_2}
[MetricSpace E]
[MetricSpace F]
(f : D T E)
(g : C(↑(Set.Icc 0 T), F))
:
The pair path (f, g) of a càdlàg path with values in E and a continuous path with
values in F.
Equations
Instances For
@[simp]
theorem
BGW.Skorokhod.prodWithCont_apply
{T : ℝ}
{E : Type u_1}
{F : Type u_2}
[MetricSpace E]
[MetricSpace F]
(f : D T E)
(g : C(↑(Set.Icc 0 T), F))
(t : ↑(Set.Icc 0 T))
:
theorem
BGW.Skorokhod.continuous_prodWithCont
{T : ℝ}
{E : Type u_1}
{F : Type u_2}
[MetricSpace E]
[MetricSpace F]
:
Continuous fun (p : D T E × C(↑(Set.Icc 0 T), F)) => prodWithCont p.1 p.2
prodWithCont is jointly continuous on D_T(E) × C([0,T], F) (Skorokhod J1 topology
and uniform topology).
theorem
BGW.Skorokhod.tendsto_prodCont
{T : ℝ}
{ι : Type u_1}
{l : Filter ι}
{u : ι → D T ℝ}
{f : D T ℝ}
{v : ι → C(↑(Set.Icc 0 T), ℝ)}
{g : C(↑(Set.Icc 0 T), ℝ)}
(hu : Filter.Tendsto u l (nhds f))
(hv : Filter.Tendsto v l (nhds g))
:
Filter.Tendsto (fun (i : ι) => prodCont (u i) (v i)) l (nhds (prodCont f g))
Sequential form of continuous_prodCont.