upcrossingsBefore_pos_eq — Mathlib

English

Equality of upcrossings counts under a positivity transformation: upcrossingsBefore with the shifted positive part equals upcrossingsBefore with the original f.

Русский

Где применяются преобразования с положительной частью, число восходящих совпадает с исходной величиной.

LaTeX

$$$\\mathrm{upcrossingsBefore}\\bigl(0,(b-a),\\lambda n\\omega. (f(n,\\omega)-a)^{+},N,\\omega\\bigr) = \\mathrm{upcrossingsBefore}(a,b,f,N,\\omega).$$$

Lean4

theorem upcrossingsBefore_pos_eq (hab : a < b) :
    upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N ω = upcrossingsBefore a b f N ω := by
  simp_rw [upcrossingsBefore, (crossing_pos_eq hab).1]

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