← Mathematical handbook

Rho and tau of arbitrary two-strip displacements

theorem Verification.continuous_medianWedge : Continuous medianWedge

theorem Verification.integral_medianWedge : ∫ (u : ↑unitInterval), medianWedge u = 1 / 4

theorem Verification.rho_twoStrip (g : StripDisplacement) : (twoStrip g).spearmanRho = 3 * ∫ (v : ↑unitInterval), g.toFun v

theorem Verification.twoStrip_mix_reflect_first (g : StripDisplacement) : (twoStrip g).mix ((twoStrip g).reflect {0}) ProbabilityTheory.Copula.unitHalf = ProbabilityTheory.Copula.independence 2

theorem Verification.concordanceQ_reflect_first_self (C : ProbabilityTheory.Copula 2) : C.concordanceQ (C.reflect {0}) = 0

theorem Verification.tau_twoStrip (g : StripDisplacement) : (twoStrip g).kendallTau = 2 * ∫ (v : ↑unitInterval), g.toFun v