← Mathematical handbook

Lemma 3.2: attaining the sign bound for every magnitude coupling

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thresholdSign (t : ℝ) (x : Fin 2 → ↑unitInterval) : Bool

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.thresholdSign t x = if t ≤ max ↑(x 0) ↑(x 1) then true else false

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.measurable_thresholdSign (t : ℝ) : Measurable (thresholdSign t)

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.signOptimizer (D : ProbabilityTheory.Copula 2) (t : ℝ) : ProbabilityTheory.Copula 2

Equations

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

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.signOptimizer_magnitude (D : ProbabilityTheory.Copula 2) (t : ℝ) : magnitudeCopula (signOptimizer D t) = D

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.signOptimizer_value (D : ProbabilityTheory.Copula 2) (t : ℝ) : (signOptimizer D t).spearmanRho - 3 / 2 * t * (signOptimizer D t).giniGamma = 3 * ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂D.toMeasure

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.sign_bound_attained (D : ProbabilityTheory.Copula 2) (t : ℝ) : ∃ (C : ProbabilityTheory.Copula 2), magnitudeCopula C = D ∧ C.spearmanRho - 3 / 2 * t * C.giniGamma = 3 * ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂D.toMeasure

Every uniform magnitude law has a copula that attains the pointwise sign bound.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.supporting_bound_iff_transport_bound (t v : ℝ) : (∀ (C : ProbabilityTheory.Copula 2), C.spearmanRho - 3 / 2 * t * C.giniGamma ≤ 3 * v) ↔ ∀ (D : ProbabilityTheory.Copula 2), ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂D.toMeasure ≤ v

Equality of the upper-bound problems, without assuming existence of an optimizer.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.transport_optimizer_lifts (D : ProbabilityTheory.Copula 2) (t : ℝ) (hD : ∀ (E : ProbabilityTheory.Copula 2), ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂E.toMeasure ≤ ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂D.toMeasure) (C : ProbabilityTheory.Copula 2) : C.spearmanRho - 3 / 2 * t * C.giniGamma ≤ (signOptimizer D t).spearmanRho - 3 / 2 * t * (signOptimizer D t).giniGamma

An optimal magnitude coupling yields an optimal copula with the same magnitude law.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.transport_contact_support (D : ProbabilityTheory.Copula 2) (t : ℝ) {f : ↑unitInterval → ℝ} (hf : Continuous f) (hfeasible : ∀ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ≤ f (x 0) + f (x 1)) (hcontact : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂D.toMeasure, magnitudeCost t x = f (x 0) + f (x 1)) : (∀ (C : ProbabilityTheory.Copula 2), C.spearmanRho - 3 / 2 * t * C.giniGamma ≤ 6 * ∫ (u : ↑unitInterval), f u) ∧ (signOptimizer D t).spearmanRho - 3 / 2 * t * (signOptimizer D t).giniGamma = 6 * ∫ (u : ↑unitInterval), f u

A feasible potential with contact certifies an attained supporting line.

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.transportValue (t : ℝ) : ℝ

The magnitude transport value, defined independently of any proposed optimizer.

Equations

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

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.transportValue_attained (t : ℝ) : ∃ (D : ProbabilityTheory.Copula 2), ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂D.toMeasure = transportValue t ∧ ∀ (E : ProbabilityTheory.Copula 2), ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂E.toMeasure ≤ transportValue t

Compactness supplies a genuine maximizer in equation (31).

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.supporting_maximum (t : ℝ) : IsGreatest (Set.range fun (C : ProbabilityTheory.Copula 2) => C.spearmanRho - 3 / 2 * t * C.giniGamma) (3 * transportValue t)

Equation (32), including attainment of both maxima.