← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.finite_boundary_or_endpoint {n : ℕ} (hn : 3 ≤ n) (π : Equiv.Perm (Fin n)) (u : Fin n → ℝ) (hu : ∀ (i : Fin n), 0 ≤ u i) (hs : ∑ i : Fin n, u i = 1) : ∃ (perm : Equiv.Perm (Fin n)) (v : Fin n → ℝ), (∀ (i : Fin n), 0 ≤ v i) ∧ ∑ i : Fin n, v i = 1 ∧ (permutationSigns perm).a v = (permutationSigns π).a u ∧ (permutationSigns perm).b v ≤ (permutationSigns π).b u ∧ ((∃ (i : Fin n), v i = 0) ∨ (∀ (i : Fin n), 0 < v i) ∧ ∃ (i : Fin n), ∀ (j : Fin n), j ≠ i → (permutationSigns perm).edge i j = 1)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.permutation_complete_replacement (n : ℕ) (π : Equiv.Perm (Fin n)) (u : Fin n → ℝ) (hu : ∀ (i : Fin n), 0 ≤ u i) (hs : ∑ i : Fin n, u i = 1) : CompleteReplacement (permutationSigns π) u

The finite minimization theorem: decreasing permutations suffice.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.finite_sharp_bound (n : ℕ) (π : Equiv.Perm (Fin n)) (u : Fin n → ℝ) (hu : ∀ (i : Fin n), 0 ≤ u i) (hs : ∑ i : Fin n, u i = 1) : ∃ (m : ℕ) (s : ↑unitInterval), arcTau m ↑s = 1 - 4 * (permutationSigns π).a u ∧ arcRho m ↑s ≤ 1 - 6 * (permutationSigns π).a u + 6 * (permutationSigns π).b u

The sharp lower prototype dominates every finite weighted permutation.