← Mathematical handbook

noncomputable def Verification.n10LogDen (u v t : ℝ) : ℝ

Equations

• Verification.n10LogDen u v t = Real.log (1 + (1 - Real.exp (t * Real.log u)) * (1 - Real.exp (t * Real.log v)))

theorem Verification.n10LogDen_deriv_zero (u v : ℝ) : HasDerivAt (n10LogDen u v) 0 0

theorem Verification.nelsen10_continuousAt_zero (u v : ↑unitInterval) : ContinuousAt (fun (θ : ↑unitInterval) => (nelsen10 θ).cdf ![u, v]) 0