BrownianMotion.StochasticIntegral.Jump

source

noncomputable def Function.jump {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] [TopologicalSpace E] [AddGroup E] (f : T → E) (t : T) :

The jump of a function at a point t, defined as the difference between the value of the function at that point and its left limit at the least upper bound of the set of points strictly smaller. If the point is not isolated from the left, then it is f t - leftLim f t. If the point is isolated from the left, and the l.u.b. or the strictly smaller points is s < t, then the jump is f t - f s. It there is no such point s because t is a bottom element, then the jump is 0 (since f ⊥ - leftLim f ⊥ = 0).

Equations

Function.jump f t = if h : ∃ (s : T), s ⋖ t then f t - f h.choose else f t - Function.leftLim f t

Instances For

source

def Function.termΔ :

Lean.ParserDescr

Equations

Function.termΔ = Lean.ParserDescr.node `Function.termΔ 1024 (Lean.ParserDescr.symbol "Δ")

Instances For

source

theorem jump_of_covBy {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] {f : T → E} {t : T} [AddGroup E] [TopologicalSpace E] {s : T} (h : s ⋖ t) :

Function.jump f t = f t - f s

source

@[simp]

theorem leftLim_bot {T : Type u_3} {E : Type u_4} [ConditionallyCompleteLinearOrderBot T] [TopologicalSpace E] (f : T → E) :

Function.leftLim f ⊥ = f ⊥

source

theorem jump_of_not_covBy {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] {f : T → E} {t : T} [AddGroup E] [TopologicalSpace E] (h : ∀ (s : T), ¬s ⋖ t) :

Function.jump f t = f t - Function.leftLim f t

source

theorem leftLim_add_jump_of_not_covBy {T : Type u_1} [ConditionallyCompleteLinearOrder T] {t : T} {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] {f : T → E} (h : ∀ (s : T), ¬s ⋖ t) :

Function.leftLim f t + Function.jump f t = f t

source

@[simp]

theorem jump_zero {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] {t : T} [TopologicalSpace T] [OrderTopology T] [AddGroup E] [TopologicalSpace E] [T2Space E] :

Function.jump (fun (x : T) => 0) t = 0

source

@[simp]

theorem jump_zero' {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] {t : T} [TopologicalSpace T] [OrderTopology T] [AddGroup E] [TopologicalSpace E] [T2Space E] :

Function.jump 0 t = 0

source

theorem leftLim_congr' {T : Type u_1} [ConditionallyCompleteLinearOrder T] {t : T} [TopologicalSpace T] [OrderTopology T] {E : Type u_3} [TopologicalSpace E] [T2Space E] {f g : T → E} (h_ne_bot : nhdsWithin t (Set.Iio t) ≠ ⊥) (h : f =ᶠ[nhdsWithin t (Set.Iio t)] g) (ht : f t = g t) :

Function.leftLim f t = Function.leftLim g t

source

theorem leftLim_congr {T : Type u_1} [ConditionallyCompleteLinearOrder T] {t : T} [TopologicalSpace T] [OrderTopology T] {E : Type u_3} [TopologicalSpace E] [T2Space E] {f g : T → E} (h : ∀ s ≤ t, f s = g s) :

Function.leftLim f t = Function.leftLim g t

source

theorem jump_congr {T : Type u_1} [ConditionallyCompleteLinearOrder T] {t : T} [TopologicalSpace T] [OrderTopology T] {E : Type u_3} [AddGroup E] [TopologicalSpace E] [T2Space E] {f g : T → E} (h : ∀ s ≤ t, f s = g s) :

Function.jump f t = Function.jump g t

source

@[simp]

theorem jump_of_isBot {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] {f : T → E} {t : T} [TopologicalSpace T] [OrderTopology T] [AddGroup E] [TopologicalSpace E] (h : IsBot t) :

Function.jump f t = 0

source

theorem jump_bot {E : Type u_2} [AddGroup E] [TopologicalSpace E] {T : Type u_3} [ConditionallyCompleteLinearOrderBot T] [TopologicalSpace T] [OrderTopology T] {f : T → E} :

Function.jump f ⊥ = 0

source

theorem jump_of_nhdsLT_ne_bot {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] {f : T → E} {t : T} [TopologicalSpace T] [OrderTopology T] [AddGroup E] [TopologicalSpace E] (h : nhdsWithin t (Set.Iio t) ≠ ⊥) :

Function.jump f t = f t - Function.leftLim f t

source

theorem jump_of_nhdsLT_neBot {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] {f : T → E} {t : T} [TopologicalSpace T] [OrderTopology T] [AddGroup E] [TopologicalSpace E] [h : (nhdsWithin t (Set.Iio t)).NeBot] :

Function.jump f t = f t - Function.leftLim f t

source

theorem leftLim_add_jump_of_ne_bot {T : Type u_1} [ConditionallyCompleteLinearOrder T] {t : T} [TopologicalSpace T] [OrderTopology T] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] {f : T → E} (h : nhdsWithin t (Set.Iio t) ≠ ⊥) :

Function.leftLim f t + Function.jump f t = f t

source

@[simp]

theorem jump_nat {E : Type u_2} [AddGroup E] [TopologicalSpace E] {f : ℕ → E} (n : ℕ) :

Function.jump f n = f n - f (n - 1)

source

theorem jump_eq_zero_of_tendsto {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] {f : T → E} {t : T} [TopologicalSpace T] [OrderTopology T] [AddGroup E] [TopologicalSpace E] [T2Space E] (h : nhdsWithin t (Set.Iio t) ≠ ⊥) (h' : Filter.Tendsto f (nhdsWithin t (Set.Iio t)) (nhds (f t))) :

Function.jump f t = 0

source

theorem ContinuousWithinAt.jump_eq_zero {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] {f : T → E} {t : T} [TopologicalSpace T] [OrderTopology T] [AddGroup E] [TopologicalSpace E] [T2Space E] (h' : nhdsWithin t (Set.Iio t) ≠ ⊥) (h : ContinuousWithinAt f (Set.Iic t) t) :

Function.jump f t = 0

source

theorem ContinuousAt.jump_eq_zero {T : Type u_1} {E : Type u_2} [ConditionallyCompleteLinearOrder T] {f : T → E} {t : T} [TopologicalSpace T] [OrderTopology T] [AddGroup E] [TopologicalSpace E] [T2Space E] (h' : nhdsWithin t (Set.Iio t) ≠ ⊥) (h : ContinuousAt f t) :

Function.jump f t = 0