Layer-cake counting for families of natural numbers

For a family k of natural numbers indexed by a finite set s, slice the values at every level j and count the indices above it, Nⱼ = #{i ∈ s | j < kᵢ}. Each index is counted once at every level below its value, so ∑ⱼ Nⱼ = ∑ᵢ kᵢ, and each pair of indices is counted together at every level below both values, so ∑ⱼ Nⱼ² = ∑_{i, i'} min kᵢ k_{i'}.

Combining the two gives the exponent identity behind the Conway–Sloane form of the local density of a diagonal Jordan form diag(uᵢ pᵏⁱ) at an odd prime: the exponent ∑ⱼ binom(Nⱼ + 1, 2) of the density, doubled, plus the exponent ∑_{i, i'} (k_{i'} - kᵢ)⁺ of the cross terms of the p-mass, is (n + 1) ∑ kᵢ.

Main results

• Finset.sum_range_card_filter_lt: ∑_{j < K} #{i ∈ s | j < kᵢ} = ∑_{i ∈ s} kᵢ when every kᵢ is at most K.
• Finset.sum_range_card_filter_lt_mul_self: ∑_{j < K} #{i ∈ s | j < kᵢ}² = ∑_{i, i' ∈ s} min kᵢ k_{i'} under the same bound.
• Finset.two_mul_sum_range_choose_add_sum_sum_tsub: 2 ∑_{j < max k} binom(Nⱼ + 1, 2) + ∑_{i, i'} (k_{i'} - kᵢ) = (#s + 1) ∑ kᵢ.

theorem Finset.sum_range_card_filter_lt {ι : Type u_1} (s : Finset ι) (k : ι → ℕ) {K : ℕ} (hK : ∀ i ∈ s, k i ≤ K) : ∑ j ∈ range K, {i ∈ s | j < k i}.card = ∑ i ∈ s, k i

Layer-cake counting. If every kᵢ with i ∈ s is at most K, then counting at each level j < K the indices with j < kᵢ gives ∑_{i ∈ s} kᵢ.

theorem Finset.sum_range_card_filter_lt_mul_self {ι : Type u_1} (s : Finset ι) (k : ι → ℕ) {K : ℕ} (hK : ∀ i ∈ s, k i ≤ K) : ∑ j ∈ range K, {i ∈ s | j < k i}.card * {i ∈ s | j < k i}.card = ∑ i ∈ s, ∑ i' ∈ s, min (k i) (k i')

Layer-cake counting for pairs. If every kᵢ with i ∈ s is at most K, then the sum over the levels j < K of the squared number of indices with j < kᵢ is ∑_{i, i' ∈ s} min kᵢ k_{i'}.

theorem Finset.two_mul_sum_range_choose_add_sum_sum_tsub {ι : Type u_1} (s : Finset ι) (k : ι → ℕ) : 2 * ∑ j ∈ range (s.sup k), ({i ∈ s | j < k i}.card + 1).choose 2 + ∑ i ∈ s, ∑ i' ∈ s, (k i' - k i) = (s.card + 1) * ∑ i ∈ s, k i

The Conway–Sloane exponent identity. Twice ∑_{j < max k} binom(Nⱼ + 1, 2), where Nⱼ = #{i ∈ s | j < kᵢ}, plus ∑_{i, i' ∈ s} (k_{i'} - kᵢ) (truncated subtraction) is (#s + 1) ∑_{i ∈ s} kᵢ. The first sum is the exponent of p in the local density of the diagonal Jordan form diag(uᵢ pᵏⁱ) at an odd prime, the second is the exponent of √p in the cross terms of its Conway–Sloane p-mass.