@[instance_reducible]

instance ProbabilityTheory.instBoundedOrderOfOrderTopOfOrderBot_brownianMotion {ι : Type u_3} [LE ι] [OrderTop ι] [OrderBot ι] : BoundedOrder ι

Equations

• ProbabilityTheory.instBoundedOrderOfOrderTopOfOrderBot_brownianMotion = { toOrderTop := inst✝¹, toOrderBot := inst✝ }

theorem ProbabilityTheory.isLocalizingSequence_leastGE {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_3} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [PolishSpace ι] (𝓕 : MeasureTheory.Filtration ι mΩ) {X : ι → Ω → ℝ} (hX1 : MeasureTheory.StronglyAdapted 𝓕 X) (hX2 : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) [𝓕.IsComplete P] [𝓕.IsRightContinuous] [MeasureTheory.IsFiniteMeasure P] : IsLocalizingSequence 𝓕 (fun (n : ℕ) => MeasureTheory.leastGE X ↑n) P

noncomputable def ProbabilityTheory.stoppedAtNorm {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {ι : Type u_3} [ConditionallyCompleteLinearOrderBot ι] (X : ι → Ω → E) (r : ℝ) : ι → Ω → E

The stopped process at the time when the norm of the process first exceeds a threshold.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ProbabilityTheory.stoppedAtNorm_of_nonpos {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {ι : Type u_3} [ConditionallyCompleteLinearOrderBot ι] (X : ι → Ω → E) {r : ℝ} (hr : r ≤ 0) : stoppedAtNorm X r = fun (x : ι) (x_1 : Ω) => 0

theorem WithBot.unbotA_inj {α : Type u_3} [Nonempty α] {a b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) : a.unbotA = b.unbotA ↔ a = b

theorem WithTop.untopA_inj {α : Type u_3} [Nonempty α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a.untopA = b.untopA ↔ a = b

@[simp]

theorem WithBot.coe_unbotA {α : Type u_3} [Nonempty α] {x : WithBot α} (hx : x ≠ ⊥) : ↑x.unbotA = x

@[simp]

theorem WithTop.coe_untopA {α : Type u_3} [Nonempty α] {x : WithTop α} (hx : x ≠ ⊤) : ↑x.untopA = x

theorem ProbabilityTheory.stoppedAtNorm_le_add_jump {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {ι : Type u_3} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {X : ι → Ω → E} (h_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) (t : ι) (ω : Ω) {n : ℝ} (hn : 0 ≤ n) : ‖stoppedAtNorm X n t ω‖ ≤ n + ‖Function.jump (fun (x : ι) => X x ω) (MeasureTheory.leastGE (fun (i : ι) (ω : Ω) => ‖X i ω‖) n ω).untopA‖