English
Under a monotone control on f, and positivity of u, a condensed sum bound holds comparing sums of f at u(k) with shifted indices.
Русский
При монотонном контроле над f и положительности u выполняется сжатое неравенство сумм, сопоставляющее суммы f(u(k)) и смещённые индексы.
LaTeX
$$$\\forall hf,\\forall n,\\; (\\sum_{k=0}^{n-1} f(k)) ≤ \\sum_{k=0}^{n-1} 2^k f(2^k)$$$
Lean4
theorem sum_condensed_le' (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) (n : ℕ) :
(∑ k ∈ range n, 2 ^ k • f (2 ^ (k + 1))) ≤ ∑ k ∈ Ico 2 (2 ^ n + 1), f k :=
by
convert sum_schlomilch_le' hf (fun n => pow_pos zero_lt_two n) (fun m n hm => pow_right_mono₀ one_le_two hm) n using 2
simp [pow_succ, mul_two]
