← Mathematical handbook

Table 1: the two-sided Frank independence limit

theorem Papers.AnsariRockel2024.frankSigned_cdf_regular (θ : ℝ) (u v : ↑unitInterval) : (frankSigned θ).cdf ![u, v] = Verification.frankRegularCDF (↑u) (↑v) θ

theorem Papers.AnsariRockel2024.frank_continuousAt_zero (u : Fin 2 → ↑unitInterval) : ContinuousAt (fun (θ : ℝ) => (frankSigned θ).cdf u) 0

theorem Papers.AnsariRockel2024.frank_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hlim : Filter.Tendsto θ l (nhds 0)) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (z : α) => (frankSigned (θ z)).cdf u) l (nhds ((ProbabilityTheory.Copula.independence 2).cdf u))