A strict majorization criterion for staircase sequences

This file identifies an integer sequence from three numerical properties: it is antitone, it is majorized by the finite staircase N - 1, ..., 0, and it has the same value as that staircase under a particular quadratic weighted sum.

The criterion is intended for uniqueness arguments in which prefix inequalities alone leave many possible sequences, but equality of a strictly convex statistic forces the extremal staircase. Its integer-valued statement applies directly to occupation-number tuples after passing between finite indices and natural-number ranges.

Main result

• TauCeti.eq_staircase_of_antitone_of_prefix_sum_le_of_sum_eq_of_casimir_eq: an antitone integer sequence satisfying the staircase prefix, total, and quadratic-sum conditions agrees with the staircase throughout the prescribed range.

References

• G. H. Hardy, J. E. Littlewood, G. Pólya, Inequalities, Cambridge University Press (1952), Chapter 2, for majorization and summation by parts.

theorem TauCeti.eq_staircase_of_antitone_of_prefix_sum_le_of_sum_eq_of_casimir_eq {N : ℕ} (a : ℕ → ℤ) (ha : ∀ (i : ℕ), i + 1 < N → a (i + 1) ≤ a i) (hmajor : ∀ k < N, ∑ i ∈ Finset.range k, a i ≤ ∑ i ∈ Finset.range k, ↑(N - (i + 1))) (hsum : ∑ i ∈ Finset.range N, a i = ∑ i ∈ Finset.range N, ↑(N - (i + 1))) (hcasimir : ∑ i ∈ Finset.range N, a i * (a i + ↑N - 2 * ↑i) = ∑ i ∈ Finset.range N, ↑(N - (i + 1)) * (↑(N - (i + 1)) + ↑N - 2 * ↑i)) (i : ℕ) : i < N → a i = ↑(N - (i + 1))

A sequence majorized by the finite staircase and having its quadratic sum is that staircase.

Let a : ℕ → ℤ be weakly decreasing through the first N entries. Suppose every proper initial sum of a is at most that of i ↦ N - (i + 1), and suppose their total sums agree. If they also have the same value under

a ↦ ∑ i < N, a i * (a i + N - 2i),

then their first N entries agree. No sign condition on a is needed.