← Mathematical handbook

The attained concave upper envelope and the complete inner enclosure

noncomputable def Papers.AnsariRockel2026RhoFootrule.upperInnerRatio (x : ℝ) : ℝ

The exact supremum in equation (45); attainment is proved below.

Equations

• Papers.AnsariRockel2026RhoFootrule.upperInnerRatio x = sSup {y : ℝ | (x, y) ∈ (convexHull ℝ) Papers.AnsariRockel2026RhoFootrule.upperSeeds}

theorem Papers.AnsariRockel2026RhoFootrule.upperInnerRatio_isGreatest (x : ℝ) (hx : x ∈ Set.Icc 0 1) : IsGreatest {y : ℝ | (x, y) ∈ (convexHull ℝ) upperSeeds} (upperInnerRatio x)

The maximum defining the source upper inner boundary exists at every x.

theorem Papers.AnsariRockel2026RhoFootrule.upper_inner_attained (x : ℝ) (hx : x ∈ Set.Icc 0 1) : ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = x ∧ copulaCorrelationRatio C = upperInnerRatio x

The upper ordinate is attained by a genuine copula.

theorem Papers.AnsariRockel2026RhoFootrule.upperInnerRatio_mem (x : ℝ) (hx : x ∈ Set.Icc 0 1) : upperInnerRatio x ∈ Set.Icc 0 1

theorem Papers.AnsariRockel2026RhoFootrule.upper_inner_concave : ConcaveOn ℝ (Set.Icc 0 1) upperInnerRatio

Concavity of the upper boundary follows from its attained convex-hull maxima.

theorem Papers.AnsariRockel2026RhoFootrule.le_upperInnerRatio (x : ℝ) (hx : x ∈ Set.Icc 0 1) : x ≤ upperInnerRatio x

The envelope is at least the diagonal, since its seed set contains (0,0) and (1,1).

theorem Papers.AnsariRockel2026RhoFootrule.lowerInnerRatio_le_self (x : ℝ) (hx : x ∈ Set.Icc 0 1) : lowerInnerRatio x ≤ x

theorem Papers.AnsariRockel2026RhoFootrule.inner_curve_order (x : ℝ) (hx : x ∈ Set.Icc 0 1) : lowerInnerRatio x ≤ upperInnerRatio x

The two attained constructions are ordered at every horizontal coordinate.

theorem Papers.AnsariRockel2026RhoFootrule.full_inner_enclosure (x y : ℝ) (hx : x ∈ Set.Icc 0 1) (hy : y ∈ Set.Icc (lowerInnerRatio x) (upperInnerRatio x)) : ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = x ∧ copulaCorrelationRatio C = y

Proposition 2.10, equation (46): every point of the entire inner enclosure is attained.