English
The oscillation of f at x is zero if and only if f is continuous at x.
Русский
Осцилляция f в точке x равна нулю тогда и только тогда, когда f непрерывна в точке x.
LaTeX
$$$\\operatorname{oscillation}(f,x)=0 \\iff \\operatorname{ContinuousAt}(f,x)$$$
Lean4
theorem sum_schlomilch_le {C : ℕ} (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ n, 0 < u n)
(h_nonneg : ∀ n, 0 ≤ f n) (hu : Monotone u) (h_succ_diff : SuccDiffBounded C u) (n : ℕ) :
∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k) ≤ (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k :=
by
rw [sum_range_succ', add_comm]
gcongr
suffices
∑ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • ∑ k ∈ range n, ((u (k + 1) - u k) • f (u (k + 1)))
by
refine this.trans (nsmul_le_nsmul_right ?_ _)
exact sum_schlomilch_le' hf h_pos hu n
have : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • ((u (k + 1) - u k) • f (u (k + 1))) :=
by
intro k _
rw [smul_smul]
gcongr
· exact h_nonneg (u (k + 1))
exact mod_cast h_succ_diff k
convert sum_le_sum this
simp [smul_sum]
