← Copula mathematical handbook

The decreasing-permutation case of the sharp inequality

Schreyer–Paulin–Trutschnig, Lemmas 4.1–4.2. A minimizing vector has equal large coordinates and at most one smaller coordinate. Its first two rank coordinates therefore lie on one of the explicit prototype arcs.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.two_level_is_arc {k : ℕ} {r b : ℝ} (hk : 0 < k) (hb : 0 ≤ b) (hbr : b ≤ r) (hs : ↑k * r + b = 1) : ∃ (n : ℕ) (s : ↑unitInterval), arcTau n ↑s = -1 + 2 * (↑k * r ^ 2 + b ^ 2) ∧ arcRho n ↑s = -1 + 2 * (↑k * r ^ 3 + b ^ 3)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.decreasing_permutation_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) (hs : ∑ i : ι, u i = 1) : ∃ (n : ℕ) (s : ↑unitInterval), arcTau n ↑s = -1 + 2 * ∑ i : ι, u i ^ 2 ∧ arcRho n ↑s ≤ -1 + 2 * ∑ i : ι, u i ^ 3