← Mathematical handbook

theorem Verification.rafteryDensity_nonneg {a : ℝ} (ha : 1 ≤ a) (u v : ↑unitInterval) : 0 ≤ rafteryDensity a ↑u ↑v

theorem Verification.rafteryDensity_continuousAt {a u v : ℝ} (hu : 0 < u) (hv : 0 < v) : ContinuousAt (Function.uncurry (rafteryDensity a)) (u, v)

theorem Verification.rafteryF_eq_cdf {a : ℝ} (ha : 1 < a) (u v : ↑unitInterval) : rafteryF a ↑u ↑v = (rafteryPower a ha).cdf ![u, v]

theorem Verification.rafteryPower_toMeasure_density {a : ℝ} (ha : 1 < a) : (rafteryPower a ha).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (rafteryDensity a ↑(x 0) ↑(x 1))

theorem Verification.raftery_toMeasure_density (δ : ↑unitInterval) (h1 : δ ≠ 1) : (raftery δ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (rafteryDensity (1 / (1 - ↑δ)) ↑(x 0) ↑(x 1))

theorem Verification.raftery_absolutelyContinuous (δ : ↑unitInterval) (h1 : δ ≠ 1) : (raftery δ).toMeasure.AbsolutelyContinuous MeasureTheory.volume