← Mathematical handbook

theorem Verification.frank_cdf_lower_bound (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : min ↑u ↑v - Real.log 2 / θ ≤ (ProbabilityTheory.Copula.frank θ hθ).cdf ![u, v]

theorem Verification.tendsto_frank_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (z : α), 0 < θ z) (hlim : Filter.Tendsto θ l Filter.atTop) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (z : α) => (ProbabilityTheory.Copula.frank (θ z) ⋯).cdf u) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))

theorem Verification.tendsto_frankNegative_atBot {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (z : α), θ z < 0) (hlim : Filter.Tendsto θ l Filter.atBot) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (z : α) => (ProbabilityTheory.Copula.frankNegative (θ z) ⋯).cdf u) l (nhds (ProbabilityTheory.Copula.countermonotonic.cdf u))