English
If f is a filtration over Nat, then ω ↦ τ(ω) + i is a stopping time for any i ∈ Nat.
Русский
Если фильтрация задана над Nat, то ω ↦ τ(ω) + i является остановочным временем для любого i ∈ Nat.
LaTeX
$$$\forall i \in \mathbb{N},\ \text{IsStoppingTime}(f, \lambda \omega. \tau(\omega) + i)$$$
Lean4
theorem add_const_nat {f : Filtration ℕ m} {τ : Ω → ℕ} (hτ : IsStoppingTime f τ) {i : ℕ} :
IsStoppingTime f fun ω => τ ω + i :=
by
refine isStoppingTime_of_measurableSet_eq fun j => ?_
by_cases hij : i ≤ j
· simp_rw [eq_comm, ← Nat.sub_eq_iff_eq_add hij, eq_comm]
exact f.mono (j.sub_le i) _ (hτ.measurableSet_eq (j - i))
· rw [not_le] at hij
convert @MeasurableSet.empty _ (f.1 j)
ext ω
simp only [Set.mem_empty_iff_false, iff_false, Set.mem_setOf]
cutsat
-- generalize to certain countable type?
