← Mathematical handbook

theorem Verification.raftery_comonotonic_bounds (δ u v : ↑unitInterval) : min ↑u ↑v - (1 - ↑δ) ≤ (raftery δ).cdf ![u, v] ∧ (raftery δ).cdf ![u, v] ≤ min ↑u ↑v

A uniform CDF error bound at the comonotonic endpoint.

theorem Verification.raftery_tendsto_one {A : Type u_1} {l : Filter A} (δ : A → ↑unitInterval) (hδ : Filter.Tendsto (fun (x : A) => ↑(δ x)) l (nhds 1)) (u v : ↑unitInterval) : Filter.Tendsto (fun (x : A) => (raftery (δ x)).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf ![u, v]))

theorem Verification.raftery_tendsto_parameter {A : Type u_1} {l : Filter A} (δ : A → ↑unitInterval) (η : ↑unitInterval) (hδ : Filter.Tendsto (fun (x : A) => ↑(δ x)) l (nhds ↑η)) (u v : ↑unitInterval) : Filter.Tendsto (fun (x : A) => (raftery (δ x)).cdf ![u, v]) l (nhds ((raftery η).cdf ![u, v]))

Continuous parameter dependence on the entire closed parameter interval and closed square.

theorem Verification.raftery_tendsto_zero {A : Type u_1} {l : Filter A} (δ : A → ↑unitInterval) (hδ : Filter.Tendsto (fun (x : A) => ↑(δ x)) l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (x : A) => (raftery (δ x)).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.independence 2).cdf ![u, v]))