variationOnFromTo — Mathlib

English

The variation of f on the diagonal equals zero: variationOnFromTo f s a a = 0 for any a ∈ s.

Русский

Вариация на самой точке равна нулю: variationOnFromTo f s a a = 0.

LaTeX

$$$\\text{variationOnFromTo}\\ f\\ s\\ a\\ a = 0$$

Lean4

/-- The **signed** variation of `f` on the interval `Icc a b` intersected with the set `s`,
squashed to a real (therefore only really meaningful if the variation is finite)
-/
noncomputable def variationOnFromTo (f : α → E) (s : Set α) (a b : α) : ℝ :=
  if a ≤ b then (eVariationOn f (s ∩ Icc a b)).toReal else -(eVariationOn f (s ∩ Icc b a)).toReal

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