← Copula mathematical handbook

An explicit trivariate copula with small Spearman's rho

We construct an explicit 3-copula witness with ∫ witness dΠ = 247/4500, hence ρ₃(witness) = 8 · 247/4500 - 1 = -631/1125 ≈ -0.560889 (multivariateSpearmanRho_witness). Together with the dual bound of Copula.Multivariate.SpearmanInfimumThree this gives

-0.56158 ≤ inf { ρ₃(C) } ≤ -631/1125 (spearmanRho_three_infimum_bounds).

The construction

Let T be uniform on [0, 1] and

• G(t) = 1 - t on [0, 1/3], 2t - 2/3 on (1/3, 7/15], t - 1/5 on (7/15, 2/3], 2t - 4/3 on (2/3, 4/5], t - 1/3 on (4/5, 1] (witnessReal);
• R(t) = t + 2/3 (mod 1) (rotReal).

Both preserve the uniform distribution (measurePreserving_witnessMap, measurePreserving_rotMap), so U = (G(T), G(R(T)), G(R(R(T)))) has uniform marginals; its law is witness. The support consists of six segments: the three tail segments (1 - y, 2y, 2y), y ∈ [0, 2/15] (and cyclic permutations), which are the exact tail structure of the Bernard–Jiang–Wang minimizer with c = 2/15, and three middle segments on the cells of [4/15, 13/15] cut into thirds, each comonotone in two coordinates and countermonotone in the third. This is the optimum among such block designs with five cells per axis (found by linear programming); the exact infimum ≈ -0.5615741 would require a joint mix in the middle.

The proof that G and R preserve Lebesgue measure checks ∫₀¹ ψ(G t) dt = ∫₀¹ ψ for continuous ψ piece by piece (affine change of variables), which identifies the image measure through integrals of bounded continuous functions.

Measure-preserving piecewise affine maps

theorem ProbabilityTheory.Copula.SpearmanInfimum.measurePreserving_of_integral_comp {g : ↑unitInterval → ↑unitInterval} {G : ℝ → ℝ} (hg : Measurable g) (hgG : ∀ (t : ↑unitInterval), ↑(g t) = G ↑t) (hG : ∀ (ψ : ℝ → ℝ), Continuous ψ → ∫ (t : ℝ) in 0..1, ψ (G t) = ∫ (x : ℝ) in 0..1, ψ x) : MeasureTheory.MeasurePreserving g MeasureTheory.volume MeasureTheory.volume

A real map G restricting to a self-map g of [0,1] preserves Lebesgue measure as soon as ∫₀¹ ψ(G t) dt = ∫₀¹ ψ for every continuous ψ.

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.rotReal (t : ℝ) : ℝ

The rotation R(t) = t + 2/3 (mod 1) on [0, 1].

Equations

• ProbabilityTheory.Copula.SpearmanInfimum.rotReal t = if t ≤ 1 / 3 then t + 2 / 3 else t - 1 / 3

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.witnessReal (t : ℝ) : ℝ

The piecewise affine map G.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.SpearmanInfimum.measurable_rotReal : Measurable rotReal

theorem ProbabilityTheory.Copula.SpearmanInfimum.measurable_witnessReal : Measurable witnessReal

theorem ProbabilityTheory.Copula.SpearmanInfimum.rotReal_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) : rotReal t ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.SpearmanInfimum.witnessReal_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) : witnessReal t ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.SpearmanInfimum.integral_comp_rotReal (ψ : ℝ → ℝ) (hψ : Continuous ψ) : ∫ (t : ℝ) in 0..1, ψ (rotReal t) = ∫ (x : ℝ) in 0..1, ψ x

theorem ProbabilityTheory.Copula.SpearmanInfimum.integral_comp_witnessReal (ψ : ℝ → ℝ) (hψ : Continuous ψ) : ∫ (t : ℝ) in 0..1, ψ (witnessReal t) = ∫ (x : ℝ) in 0..1, ψ x

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.rotMap (t : ↑unitInterval) : ↑unitInterval

R as a self-map of [0, 1].

Equations

• ProbabilityTheory.Copula.SpearmanInfimum.rotMap t = Set.projIcc 0 1 ProbabilityTheory.Copula.SpearmanInfimum.rotMap._proof_1 (ProbabilityTheory.Copula.SpearmanInfimum.rotReal ↑t)

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.witnessMap (t : ↑unitInterval) : ↑unitInterval

G as a self-map of [0, 1].

Equations

• ProbabilityTheory.Copula.SpearmanInfimum.witnessMap t = Set.projIcc 0 1 ProbabilityTheory.Copula.SpearmanInfimum.rotMap._proof_1 (ProbabilityTheory.Copula.SpearmanInfimum.witnessReal ↑t)

theorem ProbabilityTheory.Copula.SpearmanInfimum.coe_rotMap (t : ↑unitInterval) : ↑(rotMap t) = rotReal ↑t

theorem ProbabilityTheory.Copula.SpearmanInfimum.coe_witnessMap (t : ↑unitInterval) : ↑(witnessMap t) = witnessReal ↑t

theorem ProbabilityTheory.Copula.SpearmanInfimum.measurePreserving_rotMap : MeasureTheory.MeasurePreserving rotMap MeasureTheory.volume MeasureTheory.volume

theorem ProbabilityTheory.Copula.SpearmanInfimum.measurePreserving_witnessMap : MeasureTheory.MeasurePreserving witnessMap MeasureTheory.volume MeasureTheory.volume

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.witnessCoord : Fin 3 → ↑unitInterval → ↑unitInterval

The three coordinate maps G, G ∘ R, G ∘ R ∘ R.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.SpearmanInfimum.measurePreserving_witnessCoord (i : Fin 3) : MeasureTheory.MeasurePreserving (witnessCoord i) MeasureTheory.volume MeasureTheory.volume

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.witness : Copula 3

The explicit witness copula: the law of (G(T), G(R(T)), G(R(R(T)))), T uniform.

Equations

• One or more equations did not get rendered due to their size.

The value of ∫ witness dΠ

noncomputable def ProbabilityTheory.Copula.SpearmanInfimum.witnessIntegrand (t : ℝ) : ℝ

The integrand F(t) = (1 - G t)(1 - G(R t))(1 - G(R(R t))).

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.SpearmanInfimum.integral_witness_eq : ∫ (u : Fin 3 → ↑unitInterval), witness.cdf u ∂(independence 3).toMeasure = ∫ (t : ℝ) in 0..1, witnessIntegrand t

theorem ProbabilityTheory.Copula.SpearmanInfimum.integral_cdf_witness : ∫ (u : Fin 3 → ↑unitInterval), witness.cdf u ∂(independence 3).toMeasure = 247 / 4500

∫ witness dΠ = 247/4500.

theorem ProbabilityTheory.Copula.SpearmanInfimum.multivariateSpearmanRho_witness : witness.multivariateSpearmanRho = -631 / 1125

ρ₃(witness) = -631/1125 ≈ -0.560889.

theorem ProbabilityTheory.Copula.SpearmanInfimum.spearmanRho_three_infimum_bounds : (∀ (C : Copula 3), -0.56158 ≤ C.multivariateSpearmanRho) ∧ ∃ (C : Copula 3), C.multivariateSpearmanRho = -631 / 1125

Bounds for the infimum of trivariate Spearman's rho: every 3-copula has ρ₃ ≥ -0.56158, and the explicit copula witness has ρ₃ = -631/1125 ≈ -0.560889.

theorem ProbabilityTheory.Copula.SpearmanInfimum.sInf_multivariateSpearmanRho_three_mem : sInf (Set.range fun (C : Copula 3) => C.multivariateSpearmanRho) ∈ Set.Icc (-0.56158) (-631 / 1125)

The infimum of ρ₃ over all 3-copulas lies in [-0.56158, -631/1125].