cadlag functions

theorem IsRightContinuous.comp_of_monotone_of_continuous {ι : Type u_1} {E : Type u_2} [TopologicalSpace ι] {κ : Type u_3} [LinearOrder ι] [PartialOrder κ] [TopologicalSpace κ] [TopologicalSpace E] {f : κ → E} (hf : IsRightContinuous f) {ψ : ι → κ} (hψ : Monotone ψ) (hψc : Continuous ψ) : IsRightContinuous (f ∘ ψ)

The composition of a right-continuous function with a monotone continuous function is right-continuous.

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.inv {ι : Type u_1} [TopologicalSpace ι] {E : Type u_3} [Inv E] [TopologicalSpace E] [ContinuousInv E] [Preorder ι] {f : ι → E} (hf : IsCadlag f) : IsCadlag f⁻¹

theorem IsCadlag.neg {ι : Type u_1} [TopologicalSpace ι] {E : Type u_3} [Neg E] [TopologicalSpace E] [ContinuousNeg E] [Preorder ι] {f : ι → E} (hf : IsCadlag f) : IsCadlag (-f)

theorem IsCadlag.fun_inv {ι : Type u_1} [TopologicalSpace ι] {E : Type u_3} [Inv E] [TopologicalSpace E] [ContinuousInv E] [Preorder ι] {f : ι → E} (hf : IsCadlag f) : IsCadlag fun (i : ι) => (f i)⁻¹

Eta-expanded form of IsCadlag.inv

theorem IsCadlag.fun_neg {ι : Type u_1} [TopologicalSpace ι] {E : Type u_3} [Neg E] [TopologicalSpace E] [ContinuousNeg E] [Preorder ι] {f : ι → E} (hf : IsCadlag f) : IsCadlag fun (i : ι) => -f i

Eta-expanded form of IsCadlag.neg

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

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 IsCadlag.comp_of_monotone_of_continuous {ι : Type u_1} {E : Type u_2} [TopologicalSpace ι] {κ : Type u_3} [LinearOrder ι] [OrderTopology ι] [PartialOrder κ] [TopologicalSpace κ] [TopologicalSpace E] {f : κ → E} (hf : IsCadlag f) {ψ : ι → κ} (hψ : Monotone ψ) (hψc : Continuous ψ) : IsCadlag (f ∘ ψ)

The composition of a càdlàg function with a monotone continuous function is càdlàg.