← Mathematical handbook

Lemma 3.1 converse: realization of a joint magnitude/sign law

The original probability space is arbitrary: the sign need not be a function of the two magnitudes. A fair simultaneous sign flip makes both ranks uniform.

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.signedLift (e s : Bool) (a b : ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.signedLift e s a b = ![Verification.signedRank e a, Verification.signedRank (if e = true then s else !s) b]

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.measurable_signedLift {Ω : Type u_1} [MeasurableSpace Ω] {A B : Ω → ↑unitInterval} {S : Ω → Bool} (hA : Measurable A) (hB : Measurable B) (hS : Measurable S) (e : Bool) : Measurable fun (w : Ω) => signedLift e (S w) (A w) (B w)

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.signCopula {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {A B : Ω → ↑unitInterval} {S : Ω → Bool} (hA : Measurable A) (hB : Measurable B) (hS : Measurable S) (hU : MeasureTheory.Measure.map A ↑μ = MeasureTheory.volume) (hV : MeasureTheory.Measure.map B ↑μ = MeasureTheory.volume) : ProbabilityTheory.Copula 2

Equations

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

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.toMeasure_signCopula {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {A B : Ω → ↑unitInterval} {S : Ω → Bool} (hA : Measurable A) (hB : Measurable B) (hS : Measurable S) (hU : MeasureTheory.Measure.map A ↑μ = MeasureTheory.volume) (hV : MeasureTheory.Measure.map B ↑μ = MeasureTheory.volume) : (signCopula μ hA hB hS hU hV).toMeasure = Verification.fairMeasure (↑μ) (fun (w : Ω) => signedLift true (S w) (A w) (B w)) fun (w : Ω) => signedLift false (S w) (A w) (B w)

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.magnitude_signedRank (s : Bool) (a : ↑unitInterval) : rankMagnitude (Verification.signedRank s a) = a

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.magnitude_signedLift (e s : Bool) (a b : ↑unitInterval) : (fun (i : Fin 2) => rankMagnitude (signedLift e s a b i)) = ![a, b]

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.sign_signedLift (e s : Bool) {a b : ↑unitInterval} (ha : 0 < ↑a) (hb : 0 < ↑b) : rankSign (signedLift e s a b) = if s = true then 1 else -1

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.measurable_rankSign : Measurable rankSign

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.rankTriple (x : Fin 2 → ↑unitInterval) : (Fin 2 → ↑unitInterval) × ℝ

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.rankTriple x = (fun (i : Fin 2) => Papers.AnsariRockelSteinmassl2026RhoGamma.rankMagnitude (x i), Papers.AnsariRockelSteinmassl2026RhoGamma.rankSign x)

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.measurable_rankTriple : Measurable rankTriple

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.signCopula_joint_law {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {A B : Ω → ↑unitInterval} {S : Ω → Bool} (hA : Measurable A) (hB : Measurable B) (hS : Measurable S) (hU : MeasureTheory.Measure.map A ↑μ = MeasureTheory.volume) (hV : MeasureTheory.Measure.map B ↑μ = MeasureTheory.volume) : MeasureTheory.Measure.map rankTriple (signCopula μ hA hB hS hU hV).toMeasure = MeasureTheory.Measure.map (fun (w : Ω) => (![A w, B w], if S w = true then 1 else -1)) ↑μ

Full joint-law converse, including random signs conditional on both magnitudes.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.signCopula_magnitude_law {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {A B : Ω → ↑unitInterval} {S : Ω → Bool} (hA : Measurable A) (hB : Measurable B) (hS : Measurable S) (hU : MeasureTheory.Measure.map A ↑μ = MeasureTheory.volume) (hV : MeasureTheory.Measure.map B ↑μ = MeasureTheory.volume) : (magnitudeCopula (signCopula μ hA hB hS hU hV)).toMeasure = MeasureTheory.Measure.map (fun (w : Ω) => ![A w, B w]) ↑μ

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.integral_signCopula {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {A B : Ω → ↑unitInterval} {S : Ω → Bool} (hA : Measurable A) (hB : Measurable B) (hS : Measurable S) (hU : MeasureTheory.Measure.map A ↑μ = MeasureTheory.volume) (hV : MeasureTheory.Measure.map B ↑μ = MeasureTheory.volume) {f : (Fin 2 → ↑unitInterval) × ℝ → ℝ} (hf : Measurable f) : ∫ (x : Fin 2 → ↑unitInterval), f (rankTriple x) ∂(signCopula μ hA hB hS hU hV).toMeasure = ∫ (w : Ω), f (![A w, B w], if S w = true then 1 else -1) ∂↑μ

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.signCopula_rho {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {A B : Ω → ↑unitInterval} {S : Ω → Bool} (hA : Measurable A) (hB : Measurable B) (hS : Measurable S) (hU : MeasureTheory.Measure.map A ↑μ = MeasureTheory.volume) (hV : MeasureTheory.Measure.map B ↑μ = MeasureTheory.volume) : (signCopula μ hA hB hS hU hV).spearmanRho = 3 * ∫ (w : Ω), (if S w = true then 1 else -1) * ↑(A w) * ↑(B w) ∂↑μ

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.signCopula_gamma {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {A B : Ω → ↑unitInterval} {S : Ω → Bool} (hA : Measurable A) (hB : Measurable B) (hS : Measurable S) (hU : MeasureTheory.Measure.map A ↑μ = MeasureTheory.volume) (hV : MeasureTheory.Measure.map B ↑μ = MeasureTheory.volume) : (signCopula μ hA hB hS hU hV).giniGamma = 2 * ∫ (w : Ω), (if S w = true then 1 else -1) * min ↑(A w) ↑(B w) ∂↑μ