← Mathematical handbook

theorem Verification.rafteryKernel_joint_measurable (a : ℝ) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => rafteryKernel a p.1 p.2

theorem Verification.rafteryKernel_coordinate_integrable {a : ℝ} (ha : 0 ≤ a) (t : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => rafteryKernel a u t) MeasureTheory.volume

theorem Verification.integral_rafteryKernel_coordinate {a : ℝ} (ha : 0 ≤ a) (t : ↑unitInterval) : ∫ (u : ↑unitInterval), rafteryKernel a u t = 1 - a * ↑t / (a + 1)

theorem Verification.integral_rafteryPower_cdf {a : ℝ} (ha : 1 < a) : ∫ (x : Fin 2 → ↑unitInterval), (rafteryPower a ha).cdf x = a * (a + 2) / (3 * (a + 1) ^ 2)

theorem Verification.rafteryPower_spearmanRho {a : ℝ} (ha : 1 < a) : (rafteryPower a ha).spearmanRho = (a - 1) * (a + 3) / (a + 1) ^ 2

theorem Verification.raftery_spearmanRho (δ : ↑unitInterval) : (raftery δ).spearmanRho = ↑δ * (4 - 3 * ↑δ) / (2 - ↑δ) ^ 2