cadlag functions

@[reducible, inline]

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

The predicate that a function is right continuous.

Equations

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

theorem Function.IsRightContinuous.continuous_comp {ι : Type u_1} {E : Type u_2} [TopologicalSpace ι] {F : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [Preorder ι] {g : E → F} {f : ι → E} (hg : Continuous g) (hf : IsRightContinuous f) : IsRightContinuous (g ∘ f)

@[simp]

theorem Function.isRightContinuous_const {ι : Type u_1} {E : Type u_2} [TopologicalSpace ι] [TopologicalSpace E] [Preorder ι] (c : E) : IsRightContinuous fun (x : ι) => c

structure IsCadlag {ι : Type u_1} {E : Type u_2} [TopologicalSpace ι] [TopologicalSpace E] [Preorder ι] (f : ι → E) : Prop

A function is cadlag if it is right-continuous and has left limits.

• right_continuous : Function.IsRightContinuous f
• left_limit (x : ι) : ∃ (l : E), Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds l)

def leftJumpSet {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] [LinearOrder ι] (f : ι → E) : Set ι

The set of left jump times of a function.

Equations

• leftJumpSet f = {t : ι | Function.leftLim f t ≠ f t}

theorem IsCadlag.leftJumpSet_eq_discontinuitySet {ι : Type u_1} {E : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] [TopologicalSpace E] [T2Space E] {f : ι → E} (hf : IsCadlag f) : leftJumpSet f = {t : ι | ¬ContinuousAt f t}

For a càdlàg function, the left jump times are exactly its discontinuity points.

def largeLeftJumpSet {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] [LinearOrder ι] (f : ι → E) (v : Set (E × E)) : Set ι

The set of large left jump times.

Equations

• largeLeftJumpSet f v = {t : ι | (f t, Function.leftLim f t) ∉ v}

theorem IsCadlag.not_accPt_largeLeftJumpSet {ι : Type u_1} {E : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] [UniformSpace E] {f : ι → E} (hf : IsCadlag f) {v : Set (E × E)} (hv : v ∈ uniformity E) (t : ι) : ¬AccPt t (Filter.principal (largeLeftJumpSet f v))

The set of large left jump times has no accumulation points. TODO: maybe to_dual can be extended to simplify this proof as the proof of the second part is very similar to the first part.

theorem IsCadlag.finite_largeLeftJumpSet {ι : Type u_1} {E : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] [CompactSpace ι] [UniformSpace E] {f : ι → E} (hf : IsCadlag f) {v : Set (E × E)} (hv : v ∈ uniformity E) : (largeLeftJumpSet f v).Finite

If ι is a compact space, then a càdlàg function has only finitely many large jumps.

theorem IsCadlag.add {ι : Type u_1} [TopologicalSpace ι] {E : Type u_3} [Add E] [TopologicalSpace E] [ContinuousAdd E] [Preorder ι] {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] [Preorder ι] {f : ι → E} (hf : IsCadlag f) (r : ℝ) : IsCadlag fun (i : ι) => r • f i

theorem IsCadlag.continuous_comp {κ : Type u_3} {E : Type u_4} {F : Type u_5} [TopologicalSpace κ] [TopologicalSpace E] [TopologicalSpace F] [Preorder κ] {g : E → F} {f : κ → E} (hg : Continuous g) (hf : IsCadlag f) : IsCadlag (g ∘ f)

theorem IsCadlag.norm_sq {κ : Type u_3} {F : Type u_4} [TopologicalSpace κ] [NormedAddCommGroup F] [Preorder κ] {f : κ → F} (hf : IsCadlag f) : IsCadlag fun (i : κ) => ‖f i‖ ^ 2

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.