stoppedValue_sub_eq_sum — Mathlib

English

For β an additive group and τ ≤ π pointwise, the stopped value difference equals the sum of increments of u from τ to π over the index set Ico(τ,π).

Русский

Пусть β — аддитивная группа и τ ≤ π покомпонентно; тогда разность stoppedValue(u,π) − stoppedValue(u,τ) равна сумме приращений функции u от τ до π по индексу Ico(τ,π).

LaTeX

$$$\text{stoppedValue } u\ π - \text{stoppedValue } u\ τ =\ \lambda \omega.\ \sum_{i \in \mathrm{Finset}.Ico(τ(ω),π(ω))} (u(i+1,ω) - u(i,ω))$$$

Lean4

theorem stoppedValue_sub_eq_sum [AddCommGroup β] (hle : τ ≤ π) :
    stoppedValue u π - stoppedValue u τ = fun ω => (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω :=
  by
  ext ω
  rw [Finset.sum_Ico_eq_sub _ (hle ω), Finset.sum_range_sub, Finset.sum_range_sub]
  simp [stoppedValue]

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