exists_monotoneOn_sub_monotoneOn — Mathlib

English

If f has LocallyBoundedVariationOn f s, then there exist monotone functions p and q on s with f = p − q.

Русский

Если f имеет LocallyBoundedVariationOn на s, то существуют монотонные функции p и q на s такие, что f = p − q.

LaTeX

$$∃ p q : α → ℝ, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q$$

Lean4

/-- If a real-valued function has bounded variation on a set, then it is a difference of monotone
functions there. -/
theorem exists_monotoneOn_sub_monotoneOn {f : α → ℝ} {s : Set α} (h : LocallyBoundedVariationOn f s) :
    ∃ p q : α → ℝ, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q :=
  by
  rcases eq_empty_or_nonempty s with (rfl | ⟨c, cs⟩)
  · exact ⟨f, 0, subsingleton_empty.monotoneOn _, subsingleton_empty.monotoneOn _, (sub_zero f).symm⟩
  ·
    exact
      ⟨_, _, variationOnFromTo.monotoneOn h cs, variationOnFromTo.sub_self_monotoneOn h cs, (sub_sub_cancel _ _).symm⟩

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