Filling the vertical fibres in the proof of Theorem 1.1 #
The endpoints must be supplied with both the prescribed footrule and beta. No assertion that pairwise bounds imply joint attainability is assumed here.
theorem
Papers.OrendayLaresRockel2026TauFootruleBeta.concordance_mixture
(C D E F : ProbabilityTheory.Copula 2)
(a b : ↑unitInterval)
:
(C.mix D a).concordanceQ (E.mix F b) = ↑a * ↑b * C.concordanceQ E + ↑a * (1 - ↑b) * C.concordanceQ F + (1 - ↑a) * ↑b * D.concordanceQ E + (1 - ↑a) * (1 - ↑b) * D.concordanceQ F
theorem
Papers.OrendayLaresRockel2026TauFootruleBeta.tau_mixture_continuous
(C D : ProbabilityTheory.Copula 2)
:
Continuous fun (a : ↑unitInterval) => (C.mix D a).kendallTau
theorem
Papers.OrendayLaresRockel2026TauFootruleBeta.fixed_footrule_beta_intermediate
(C D : ProbabilityTheory.Copula 2)
{p b t : ℝ}
(hpC : C.spearmanFootrule = p)
(hpD : D.spearmanFootrule = p)
(hbC : C.blomqvistBeta = b)
(hbD : D.blomqvistBeta = b)
(htC : C.kendallTau ≤ t)
(htD : t ≤ D.kendallTau)
:
∃ (E : ProbabilityTheory.Copula 2), E.spearmanFootrule = p ∧ E.blomqvistBeta = b ∧ E.kendallTau = t
The intermediate-value step of the constructive joint-region proof.