English
If f is monotone on s, then the variation on any subinterval is bounded by the real difference f(b) − f(a): eVariationOn f (s ∩ Icc a b) ≤ real(f(b) − f(a)).
Русский
Если f монотонна на s, то вариация на подотрезке ограничена вещественной разностью f(b) − f(a): eVariationOn f (s ∩ Icc a b) ≤ real(f(b) − f(a)).
LaTeX
$$$eVariationOn\\!f\\bigl(s \\cap Icc a b\\bigr) \\le \\operatorname{ofReal}\\bigl(f(b) - f(a)\\bigr)$$
Lean4
theorem eVariationOn_le {f : α → ℝ} {s : Set α} (hf : MonotoneOn f s) {a b : α} (as : a ∈ s) (bs : b ∈ s) :
eVariationOn f (s ∩ Icc a b) ≤ ENNReal.ofReal (f b - f a) :=
by
apply iSup_le _
rintro ⟨n, ⟨u, hu, us⟩⟩
calc
(∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) :=
by
refine Finset.sum_congr rfl fun i hi => ?_
simp only [Finset.mem_range] at hi
rw [edist_dist, Real.dist_eq, abs_of_nonneg]
exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
_ = ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) :=
by
rw [ENNReal.ofReal_sum_of_nonneg]
intro i _
exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
_ = ENNReal.ofReal (f (u n) - f (u 0)) := by rw [Finset.sum_range_sub fun i => f (u i)]
_ ≤ ENNReal.ofReal (f b - f a) := by
apply ENNReal.ofReal_le_ofReal
exact sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1)
