← Mathematical handbook

noncomputable def Verification.n17PowerSlope (x a : ℝ) : ℝ

Equations

• Verification.n17PowerSlope x a = Function.update (fun (a : ℝ) => (x ^ a - 1) / a) 0 (Real.log x) a

theorem Verification.n17PowerSlope_continuousAt {x : ℝ} (hx : 0 < x) : ContinuousAt (n17PowerSlope x) 0

theorem Verification.nelsen17_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), θ a ≠ 0) (ht : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen17 (θ a) ⋯).cdf ![u, v]) l (nhds (Real.exp (Real.log (1 + ↑u) * Real.log (1 + ↑v) / Real.log 2) - 1))