← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.weighted_chain_sum (N : ℕ) (B : ℕ → ℝ) : ∑ k ∈ Finset.range N, ((↑N - ↑k) * B k + (↑k + 1) * B (k + 1)) = ↑N * ∑ k ∈ Finset.range (N + 1), B k

Adjacent paths add to a constant density, including the two endpoints.