Total variation of a cyclically unimodal sequence #
A purely one-dimensional lemma used for the Cauchy perimeter of a convex polygon.
If a : ℤ → ℝ is m-periodic and, for every level t ≠ 0, there is at most one up-crossing
of the level t per period, then the cyclic total variation of a equals twice its range.
The proof is a layer-cake computation: the intervals [a j, a (j+1)) attached to the ascending
steps are pairwise disjoint (two of them would produce two up-crossings of a common level) and
they cover the range interval [N, M) up to the single point 0.
theorem
HumanVerification.CauchyCrofton.cyclic_sum_abs_sub
{m : ℕ}
(hm : 0 < m)
(a : ℤ → ℝ)
(hper : ∀ (j : ℤ), a (j + ↑m) = a j)
(hcross : ∀ (t : ℝ), t ≠ 0 → ∀ (j k : ℤ), a j ≤ t → t < a (j + 1) → a k ≤ t → t < a (k + 1) → ∃ (q : ℤ), k = j + q * ↑m)
{M N : ℝ}
(hMle : ∀ (j : ℤ), a j ≤ M)
(hMex : ∃ (j : ℤ), a j = M)
(hNle : ∀ (j : ℤ), N ≤ a j)
(hNex : ∃ (j : ℤ), a j = N)
:
Cyclic total variation of a unimodal sequence.