← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.adjacent_swap_lt {n : ℕ} {p q : Fin n} (hpq : ↑q = ↑p + 1) (i j : Fin n) (h : ¬(i = p ∧ j = q ∨ i = q ∧ j = p)) : (Equiv.swap p q) i < (Equiv.swap p q) j ↔ i < j

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.adjacent_extremal_opposite {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) {p q : Fin (n + 2)} (hgap : ↑q = ↑p + 1) (hp : π p = 0) (hq : π q = Fin.last (n + 1)) (i : Fin (n + 2)) (hip : i ≠ p) (hiq : i ≠ q) : (permutationSigns π).edge p i = -(permutationSigns π).edge q i

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.adjacent_extremal_flip {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) {p q : Fin (n + 2)} (hgap : ↑q = ↑p + 1) (hp : π p = 0) (hq : π q = Fin.last (n + 1)) : (permutationSigns (Equiv.trans (Equiv.swap p q) π)).relabel (Equiv.swap p q) = (permutationSigns π).flipPair p q ⋯

Swapping the adjacent minimum and maximum flips exactly one signed edge, after relabeling the weights by the same transposition.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.adjacent_extremal_improvement {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (u : Fin (n + 2) → ℝ) (hu : ∀ (i : Fin (n + 2)), 0 < u i) {p q : Fin (n + 2)} (hgap : ↑q = ↑p + 1) (hp : π p = 0) (hq : π q = Fin.last (n + 1)) (hthird : ∃ (k : Fin (n + 2)), k ≠ p ∧ k ≠ q) : ∃ (σ : Equiv.Perm (Fin (n + 2))) (w : Fin (n + 2) → ℝ), (∀ (i : Fin (n + 2)), 0 ≤ w i) ∧ ∑ i : Fin (n + 2), w i = ∑ i : Fin (n + 2), u i ∧ (permutationSigns σ).a w = (permutationSigns π).a u ∧ (permutationSigns σ).b w < (permutationSigns π).b u

A strictly positive weighted permutation with adjacent extremal entries cannot minimize b at fixed a when a third strip is present.