cadlag functions #
@[reducible, inline]
abbrev
Function.RightContinuous
{ι : Type u_1}
{E : Type u_2}
[TopologicalSpace ι]
[TopologicalSpace E]
[PartialOrder ι]
(f : ι → E)
:
The predicate that a function is right continuous.
Equations
- Function.RightContinuous f = ∀ (a : ι), ContinuousWithinAt f (Set.Ioi a) a
Instances For
theorem
Function.RightContinuous.continuous_comp
{ι : Type u_1}
{E : Type u_2}
[TopologicalSpace ι]
[TopologicalSpace E]
{F : Type u_3}
[TopologicalSpace F]
[PartialOrder ι]
{g : E → F}
{f : ι → E}
(hg : Continuous g)
(hf : RightContinuous f)
:
RightContinuous (g ∘ f)
structure
IsCadlag
{ι : Type u_1}
{E : Type u_2}
[TopologicalSpace ι]
[TopologicalSpace E]
[PartialOrder ι]
(f : ι → E)
:
A function is cadlag if it is right-continuous and has left limits.
- right_continuous : Function.RightContinuous f
- left_limit (x : ι) : ∃ (l : E), Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds l)
Instances For
theorem
isBounded_image_of_isLocallyBounded_of_isCompact
{X : Type u_3}
{Y : Type u_4}
[TopologicalSpace X]
[Bornology Y]
{s : Set X}
(hs : IsCompact s)
{f : X → Y}
(hf : ∀ (x : X), ∃ t ∈ nhds x, Bornology.IsBounded (f '' t))
:
Bornology.IsBounded (f '' s)
A locally bounded function maps a compact set to a bounded set.
theorem
isLocallyBounded_of_isCadlag
{ι : Type u_1}
[TopologicalSpace ι]
{E : Type u_3}
[LinearOrder ι]
[PseudoMetricSpace E]
{f : ι → E}
(hf : IsCadlag f)
(x : ι)
:
∃ t ∈ nhds x, Bornology.IsBounded (f '' t)
A càdlàg function is locally bounded.
theorem
isBounded_image_of_isCadlag_of_isCompact
{ι : Type u_1}
[TopologicalSpace ι]
{E : Type u_3}
[LinearOrder ι]
[PseudoMetricSpace E]
{f : ι → E}
(hf : IsCadlag f)
{s : Set ι}
(hs : IsCompact s)
:
Bornology.IsBounded (f '' s)
A càdlàg function maps compact sets to bounded sets.