upcrossingStrat — Mathlib

English

If n ≤ m and lowerCrossingTime a b f N n ω = N, then lowerCrossingTime a b f N m ω = N.

Русский

Если n ≤ m и нижнее время кроссинга равно N на позиции n, то равно и на позиции m.

LaTeX

$$$\forall n,m\; (n \le m) \Rightarrow (lowerCrossingTime(a,b,f,N,n,\omega)=N \Rightarrow lowerCrossingTime(a,b,f,N,m,\omega)=N)$$$

Lean4

/-- `upcrossingStrat a b f N n` is 1 if `n` is between a consecutive pair of lower and upper
crossings and is 0 otherwise. `upcrossingStrat` is shifted by one index so that it is adapted
rather than predictable. -/
noncomputable def upcrossingStrat (a b : ℝ) (f : ℕ → Ω → ℝ) (N n : ℕ) (ω : Ω) : ℝ :=
  ∑ k ∈ Finset.range N, (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator 1 n

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