← Mathematical handbook

Remark 2.3: an asymmetric SI equality copula

This constructs the source's example with A(v)=v/2, B(v)=(v+1)/2, and middle level v. Closed cut conventions give a monotone kernel version; the source's open intervals agree almost everywhere.

noncomputable def Papers.Rockel2026XiFootrule.asymmetricLowerCut (v : ↑unitInterval) : ↑unitInterval

Equations

• Papers.Rockel2026XiFootrule.asymmetricLowerCut v = ⟨↑v / 2, ⋯⟩

noncomputable def Papers.Rockel2026XiFootrule.asymmetricUpperCut (v : ↑unitInterval) : ↑unitInterval

Equations

• Papers.Rockel2026XiFootrule.asymmetricUpperCut v = ⟨(↑v + 1) / 2, ⋯⟩

noncomputable def Papers.Rockel2026XiFootrule.asymmetricKernel (v u : ↑unitInterval) : ℝ

Equations

• Papers.Rockel2026XiFootrule.asymmetricKernel v u = Verification.threeLevel (Papers.Rockel2026XiFootrule.asymmetricLowerCut v) (Papers.Rockel2026XiFootrule.asymmetricUpperCut v) (↑v) u

noncomputable def Papers.Rockel2026XiFootrule.asymmetricEquality : ProbabilityTheory.Copula 2

The actual copula specified by Remark 2.3's conditional-CDF profile.

Equations

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

theorem Papers.Rockel2026XiFootrule.asymmetricEquality_cdf (u v : ↑unitInterval) : asymmetricEquality.cdf ![u, v] = (1 - ↑v) * min (↑u) (↑v / 2) + ↑v * min (↑u) ((↑v + 1) / 2)

theorem Papers.Rockel2026XiFootrule.asymmetricEquality_isSI : asymmetricEquality.IsSI

theorem Papers.Rockel2026XiFootrule.asymmetricEquality_conditionalCDF (v : ↑unitInterval) : (fun (u : ↑unitInterval) => asymmetricEquality.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => (if ↑u < ↑v / 2 then 1 else 0) + ↑v * if ↑v / 2 < ↑u ∧ ↑u < (↑v + 1) / 2 then 1 else 0

theorem Papers.Rockel2026XiFootrule.asymmetricEquality_derivative (v : ↑unitInterval) : (fun (u : ↑unitInterval) => deriv (asymmetricEquality.cdfSection v) ↑u) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => (if ↑u < ↑v / 2 then 1 else 0) + ↑v * if ↑v / 2 < ↑u ∧ ↑u < (↑v + 1) / 2 then 1 else 0

theorem Papers.Rockel2026XiFootrule.asymmetricEquality_xi_eq_footrule : asymmetricEquality.chatterjeeXi = asymmetricEquality.spearmanFootrule

theorem Papers.Rockel2026XiFootrule.asymmetricEquality_coefficients : asymmetricEquality.chatterjeeXi = 1 / 2 ∧ asymmetricEquality.spearmanFootrule = 1 / 2

theorem Papers.Rockel2026XiFootrule.asymmetricEquality_asymmetry_witness : asymmetricEquality.cdf ![⟨1 / 4, ⋯⟩, ProbabilityTheory.Copula.unitHalf] = 1 / 4 ∧ asymmetricEquality.cdf ![ProbabilityTheory.Copula.unitHalf, ⟨1 / 4, ⋯⟩] = 7 / 32

Exact unequal transposed CDF values certify genuine asymmetry.

theorem Papers.Rockel2026XiFootrule.asymmetricEquality_not_exchangeable : ¬asymmetricEquality.IsExchangeable