← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.nonendpoint_improvement {n : ℕ} (hn : 0 < n) (π : Equiv.Perm (Fin (n + 2))) (u : Fin (n + 2) → ℝ) (hu : ∀ (i : Fin (n + 2)), 0 < u i) (h123 : NoIncreasingTriple π) (h3412 : No3412 π) (hfirst : π 0 ≠ Fin.last (n + 1)) (hlast : π (Fin.last (n + 1)) ≠ 0) : ∃ (σ : 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

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.first_maximum_edges {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) (h : π 0 = Fin.last n) (j : Fin (n + 1)) : j ≠ 0 → (permutationSigns π).edge 0 j = 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.last_minimum_edges {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) (h : π (Fin.last n) = 0) (j : Fin (n + 1)) : j ≠ Fin.last n → (permutationSigns π).edge (Fin.last n) j = 1