cadlag functions

@[reducible, inline]

abbrev Function.RightContinuous {ι : Type u_1} {E : Type u_2} [TopologicalSpace ι] [TopologicalSpace E] [PartialOrder ι] (f : ι → E) : Prop

The predicate that a function is right continuous.

Equations

• Function.RightContinuous f = ∀ (a : ι), ContinuousWithinAt f (Set.Ioi a) a

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) : Prop

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)

theorem IsCadlag.add {ι : Type u_1} [TopologicalSpace ι] {E : Type u_3} [Add E] [TopologicalSpace E] [ContinuousAdd E] [PartialOrder ι] {f g : ι → E} (hf : IsCadlag f) (hg : IsCadlag g) : IsCadlag (f + g)

theorem IsCadlag.const_smul {ι : Type u_1} [TopologicalSpace ι] {E : Type u_3} [SMul ℝ E] [TopologicalSpace E] [ContinuousSMul ℝ E] [PartialOrder ι] {f : ι → E} (hf : IsCadlag f) (r : ℝ) : IsCadlag fun (i : ι) => r • f i

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.