← Mathematical handbook

noncomputable def Verification.rafteryPrintedCDF (δ u v : ℝ) : ℝ

Literal Raftery expression in arXiv v3 Table 1, before correcting its coefficient.

Equations

• Verification.rafteryPrintedCDF δ u v = min u v + (1 - δ) * (u * v) ^ (1 / (1 - δ)) * (1 - max u v ^ (-(1 + δ) / (1 - δ)))

theorem Verification.rafteryPrintedCDF_half_witness : rafteryPrintedCDF (1 / 2) (7 / 8) (7 / 8) = 5985 / 8192

theorem Verification.raftery_printed_cdf_not_copula : ¬∃ (C : ProbabilityTheory.Copula 2), ∀ (u v : ↑unitInterval), C.cdf ![u, v] = rafteryPrintedCDF (1 / 2) ↑u ↑v

The literal printed formula cannot be the CDF of a copula.

theorem Verification.raftery_zero_density {C : ProbabilityTheory.Copula 2} (hC : C = ProbabilityTheory.Copula.independence 2) : C.HasMTP2Density

The declared independence endpoint has a TP2 Lebesgue density.

theorem Verification.raftery_one_upperTail {C : ProbabilityTheory.Copula 2} (hC : C = ProbabilityTheory.Copula.comonotonic 2) : C.HasUpperTailDependence 1 ∧ ¬C.HasUpperTailDependence 0

The declared comonotonic endpoint has upper-tail coefficient one, not zero.