← Mathematical handbook

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

Equations

• Verification.n11Base u v t = Real.exp (t * Real.log u) * Real.exp (t * Real.log v) - 2 * (1 - Real.exp (t * Real.log u)) * (1 - Real.exp (t * Real.log v))

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

Equations

• Verification.n11LogBase u v t = Real.log (Verification.n11Base u v t)

theorem Verification.n11Base_zero (u v : ℝ) : n11Base u v 0 = 1

theorem Verification.n11LogBase_deriv_zero (u v : ℝ) : HasDerivAt (n11LogBase u v) (Real.log u + Real.log v) 0

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