← Mathematical handbook

Every localized upper inner branch

noncomputable def Papers.AnsariRockel2026RhoFootrule.upperLocalized (n : ℕ) (a : ↑unitInterval) : ProbabilityTheory.Copula 2

The source branch number is n+1, so there is no zero-block convention.

Equations

• Papers.AnsariRockel2026RhoFootrule.upperLocalized n a = Verification.equalBlocks n (Papers.AnsariRockel2026RhoFootrule.upperBinary a)

noncomputable def Papers.AnsariRockel2026RhoFootrule.upperBranch (n : ℕ) (a : ℝ) : ℝ × ℝ

Equations

• Papers.AnsariRockel2026RhoFootrule.upperBranch n a = (1 - (1 - 2 * a ^ 2 * (3 - 4 * a)) / (↑n + 1), 1 - (1 - 12 * a ^ 2 * (1 - a) ^ 2) / (↑n + 1) ^ 2)

theorem Papers.AnsariRockel2026RhoFootrule.ordinal_directional_coefficients (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).chatterjeeXi = 1 - ↑a ^ 2 * (1 - C.chatterjeeXi) - (1 - ↑a) ^ 2 * (1 - D.chatterjeeXi) ∧ copulaCorrelationRatio (C.ordinalSum D a) = 1 - ↑a ^ 3 * (1 - copulaCorrelationRatio C) - (1 - ↑a) ^ 3 * (1 - copulaCorrelationRatio D)

The localization identities used to derive equation (120), including degenerate blocks.

theorem Papers.AnsariRockel2026RhoFootrule.equal_block_directional_coefficients (n : ℕ) (C : ProbabilityTheory.Copula 2) : (Verification.equalBlocks n C).chatterjeeXi = 1 - (1 - C.chatterjeeXi) / (↑n + 1) ∧ copulaCorrelationRatio (Verification.equalBlocks n C) = 1 - (1 - copulaCorrelationRatio C) / (↑n + 1) ^ 2

Equal localization into n+1 blocks for an arbitrary base copula.

theorem Papers.AnsariRockel2026RhoFootrule.upperLocalized_coefficients (n : ℕ) (a : ↑unitInterval) (ha : ↑a ≤ 1 / 2) : (upperLocalized n a).chatterjeeXi = (upperBranch n ↑a).1 ∧ copulaCorrelationRatio (upperLocalized n a) = (upperBranch n ↑a).2

Equation (120), with every positive block count represented.

theorem Papers.AnsariRockel2026RhoFootrule.upper_branch_attained (n : ℕ) (a : ℝ) (ha : a ∈ Set.Icc 0 (1 / 2)) : upperBranch n a ∈ directionalRegion

All upper branches are actual copula coefficient pairs.

theorem Papers.AnsariRockel2026RhoFootrule.upper_limit_attained : (1, 1) ∈ directionalRegion

The comonotonic limit point is also attained.

theorem Papers.AnsariRockel2026RhoFootrule.upper_branch_continuous (n : ℕ) : Continuous (upperBranch n)

Continuous dependence of every finite branch on its binary parameter.

def Papers.AnsariRockel2026RhoFootrule.upperSeeds : Set (ℝ × ℝ)

The source set in equation (45).

Equations

• Papers.AnsariRockel2026RhoFootrule.upperSeeds = insert (1, 1) (⋃ (n : ℕ), Papers.AnsariRockel2026RhoFootrule.upperBranch n '' Set.Icc 0 (1 / 2))

theorem Papers.AnsariRockel2026RhoFootrule.upper_seeds_attained : upperSeeds ⊆ directionalRegion

theorem Papers.AnsariRockel2026RhoFootrule.upper_convex_hull_attained : (convexHull ℝ) upperSeeds ⊆ directionalRegion