Documentation

Papers.Rockel2026XiFootrule.LTDExample

← Mathematical handbook

Remark 2.6(d): the printed matrix and a corrected LTD example #

The printed matrix has the stated ranks, but is not LTD: at (2/3,2/3) its CDF is 5/12, below 4/9. Replacing the lower block by masses 1/9,2/9,2/9,1/9 provides a genuine LTD copula with xi strictly larger than footrule.

source
noncomputable def Papers.Rockel2026XiFootrule.printedLTDExample :
ProbabilityTheory.Copula 2
Equations
Instances For
    source
    noncomputable def Papers.Rockel2026XiFootrule.correctedLTDExample :
    ProbabilityTheory.Copula 2
    Equations
    Instances For
      source
      theorem Papers.Rockel2026XiFootrule.printed_ltd_matrix :
      (Verification.LTDExample.thirdMatrix (1 / 4) ⋯).mass = !![1 / 3, 0, 0; 0, 1 / 12, 1 / 4; 0, 1 / 4, 1 / 12]

      Literal correspondence with the mass matrix printed in Remark 2.6(d).

      source
      theorem Papers.Rockel2026XiFootrule.printed_ltd_coefficients :
      printedLTDExample.chatterjeeXi = 1 / 2 ∧ printedLTDExample.spearmanFootrule = 1 / 3
      source
      theorem Papers.Rockel2026XiFootrule.printed_ltd_claim_false :
      ¬printedLTDExample.IsLTD

      The literal LTD assertion in the printed example is false.

      source
      theorem Papers.Rockel2026XiFootrule.corrected_ltd_matrix :
      (Verification.LTDExample.thirdMatrix (1 / 3) ⋯).mass = !![1 / 3, 0, 0; 0, 1 / 9, 2 / 9; 0, 2 / 9, 1 / 9]

      A corrected mass matrix giving the intended counterexample to xi<=footrule in LTD.

      source
      theorem Papers.Rockel2026XiFootrule.corrected_ltd_counterexample :
      correctedLTDExample.IsLTD ∧ correctedLTDExample.chatterjeeXi = 38 / 81 ∧ correctedLTDExample.spearmanFootrule = 10 / 27 ∧ correctedLTDExample.spearmanFootrule < correctedLTDExample.chatterjeeXi
      source
      theorem Papers.Rockel2026XiFootrule.corrected_ltd_not_si :
      ¬correctedLTDExample.IsSI