← Mathematical handbook

The binary building block of the upper inner curve

noncomputable def Papers.AnsariRockel2026RhoFootrule.upperBinary (a : ↑unitInterval) : ProbabilityTheory.Copula 2

Predictor reflection of the source binary model; both directional coefficients are unchanged.

Equations

• Papers.AnsariRockel2026RhoFootrule.upperBinary a = Verification.twoStrip (Verification.flatTentDisplacement a)

theorem Papers.AnsariRockel2026RhoFootrule.upperBinary_conditional_distribution (a v : ↑unitInterval) : (fun (u : ↑unitInterval) => (upperBinary a).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => if u ≤ ProbabilityTheory.Copula.unitHalf then ↑v + Verification.flatTent a v else ↑v - Verification.flatTent a v

The two conditional distribution functions are v plus or minus the flat-topped tent.

theorem Papers.AnsariRockel2026RhoFootrule.upperBinary_conditionalMean (a : ↑unitInterval) (ha : ↑a ≤ 1 / 2) : Verification.conditionalMean (upperBinary a) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => if u ≤ ProbabilityTheory.Copula.unitHalf then 1 / 2 - ↑a * (1 - ↑a) else 1 / 2 + ↑a * (1 - ↑a)

The exact conditional means of the two halves.

theorem Papers.AnsariRockel2026RhoFootrule.upperBinary_coefficients (a : ↑unitInterval) (ha : ↑a ≤ 1 / 2) : (upperBinary a).chatterjeeXi = 2 * ↑a ^ 2 * (3 - 4 * ↑a) ∧ copulaCorrelationRatio (upperBinary a) = 12 * ↑a ^ 2 * (1 - ↑a) ^ 2

The n=1 branch in equations (45) and (120).

theorem Papers.AnsariRockel2026RhoFootrule.upper_binary_attained (a : ℝ) (ha : a ∈ Set.Icc 0 (1 / 2)) : ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = 2 * a ^ 2 * (3 - 4 * a) ∧ copulaCorrelationRatio C = 12 * a ^ 2 * (1 - a) ^ 2

Each parameter on the first upper branch is realized by an actual copula.