A two-variable interface to the classical construction #
theorem
ProbabilityTheory.Copula.IsClassical.ofBivariate
(F : ↑unitInterval → ↑unitInterval → ℝ)
(hz₁ : ∀ (v : ↑unitInterval), F 0 v = 0)
(hz₂ : ∀ (u : ↑unitInterval), F u 0 = 0)
(ho₁ : ∀ (v : ↑unitInterval), F 1 v = ↑v)
(ho₂ : ∀ (u : ↑unitInterval), F u 1 = ↑u)
(hinc : ∀ (a b c e : ↑unitInterval), a ≤ b → c ≤ e → 0 ≤ F b e - F a e - F b c + F a c)
:
IsClassical fun (u : Fin 2 → ↑unitInterval) => F (u 0) (u 1)
Check a bivariate formula using its four boundary identities and rectangle inequality.