stoppedValue_stoppedValue_leastGE

English

For any f and stopping-time scheduling given by leastGE, the double stopped value equals the stopped value of the stopped process at leastGE f r n.

Русский

Для данного f и расписания останова, заданного leastGE, двойное остановленное значение равно остановленному значению останова процесса при leastGE f r n.

LaTeX

$$Eq (stoppedValue (fun i => stoppedValue f (leastGE f r i)) π) (stoppedValue (stoppedProcess f (leastGE f r n)) π).$$

Lean4

theorem stoppedValue_stoppedValue_leastGE (f : ℕ → Ω → ℝ) (π : Ω → ℕ) (r : ℝ) {n : ℕ} (hπn : ∀ ω, π ω ≤ n) :
    stoppedValue (fun i => stoppedValue f (leastGE f r i)) π = stoppedValue (stoppedProcess f (leastGE f r n)) π :=
  by
  ext1 ω
  simp +unfoldPartialApp only [stoppedProcess, stoppedValue]
  rw [leastGE_eq_min _ _ _ hπn]

Похожие утверждения