← Mathematical handbook

theorem Verification.rafteryPower_cdf_min {a : ℝ} (ha : 1 < a) (u v : ↑unitInterval) : (rafteryPower a ha).cdf ![u, v] = min ↑u ↑v + min ↑u ↑v ^ a * (max ↑u ↑v ^ a - max ↑u ↑v ^ (1 - a)) / (2 * a - 1)

theorem Verification.raftery_shape_gt_one (δ : ↑unitInterval) (h0 : δ ≠ 0) (h1 : δ ≠ 1) : 1 < 1 / (1 - ↑δ)

noncomputable def Verification.raftery (δ : ↑unitInterval) : ProbabilityTheory.Copula 2

The corrected Raftery copula, including its two endpoint measures.

Equations

• Verification.raftery δ = if h0 : δ = 0 then ProbabilityTheory.Copula.independence 2 else if h1 : δ = 1 then ProbabilityTheory.Copula.comonotonic 2 else Verification.rafteryPower (1 / (1 - ↑δ)) ⋯

theorem Verification.raftery_zero : raftery 0 = ProbabilityTheory.Copula.independence 2

theorem Verification.raftery_one : raftery 1 = ProbabilityTheory.Copula.comonotonic 2

theorem Verification.raftery_cdf_interior (δ : ↑unitInterval) (h0 : δ ≠ 0) (h1 : δ ≠ 1) (u v : ↑unitInterval) : (raftery δ).cdf ![u, v] = min ↑u ↑v + (1 - ↑δ) / (1 + ↑δ) * min ↑u ↑v ^ (1 / (1 - ↑δ)) * (max ↑u ↑v ^ (1 / (1 - ↑δ)) - max ↑u ↑v ^ (-↑δ / (1 - ↑δ)))

theorem Verification.raftery_cdf (δ : ↑unitInterval) (h1 : δ ≠ 1) (u v : ↑unitInterval) : (raftery δ).cdf ![u, v] = min ↑u ↑v + (1 - ↑δ) / (1 + ↑δ) * min ↑u ↑v ^ (1 / (1 - ↑δ)) * (max ↑u ↑v ^ (1 / (1 - ↑δ)) - max ↑u ↑v ^ (-↑δ / (1 - ↑δ)))

Correctly normalized full-square CDF for every parameter below the comonotonic endpoint.

theorem Verification.raftery_cdf_corrected (δ : ↑unitInterval) (h1 : δ ≠ 1) (u v : ↑unitInterval) : (raftery δ).cdf ![u, v] = min ↑u ↑v + (1 - ↑δ) / (1 + ↑δ) * (↑u * ↑v) ^ (1 / (1 - ↑δ)) * (1 - max ↑u ↑v ^ (-(1 + ↑δ) / (1 - ↑δ)))

The source CDF with its missing normalization factor restored.