← Mathematical handbook

noncomputable def Verification.n13LogBase (a b t : ℝ) : ℝ

Equations

• Verification.n13LogBase a b t = Real.log (Real.exp (t * Real.log a) + Real.exp (t * Real.log b) - 1)

theorem Verification.n13LogBase_deriv_zero (a b : ℝ) : HasDerivAt (n13LogBase a b) (Real.log a + Real.log b) 0

theorem Verification.nelsen13_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (z : α), 0 ≤ θ z) (hlim : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (z : α) => (nelsen13 (θ z) ⋯).cdf ![u, v]) l (nhds ((gumbelBarnett 1).cdf ![u, v]))