← Mathematical handbook

noncomputable def Verification.n10Base (θ v x : ℝ) : ℝ

Equations

• Verification.n10Base θ v x = 1 + (1 - x ^ θ) * (1 - v ^ θ)

noncomputable def Verification.n10Section (θ v x : ℝ) : ℝ

Equations

• Verification.n10Section θ v x = v * x * Verification.n10Base θ v x ^ (-θ⁻¹)

theorem Verification.n10Base_ge_one {θ : ℝ} (hθ : 0 ≤ θ) (v : ↑unitInterval) {x : ℝ} (hx : x ∈ Set.Icc 0 1) : 1 ≤ n10Base θ (↑v) x

theorem Verification.n10Section_deriv {θ : ℝ} (hθ : 0 < θ) (v : ↑unitInterval) {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : HasDerivAt (n10Section θ ↑v) (↑v * (2 - ↑v ^ θ) * n10Base θ (↑v) x ^ (-θ⁻¹ - 1)) x

theorem Verification.n10Section_convex {θ : ℝ} (hθ : 0 < θ) (v : ↑unitInterval) : ConvexOn ℝ (Set.Icc 0 1) (n10Section θ ↑v)

theorem Verification.nelsen10_section (θ u v : ↑unitInterval) (hθ : 0 < ↑θ) : (nelsen10 θ).cdf ![u, v] = n10Section ↑θ ↑v ↑u

theorem Verification.nelsen10_isSD (θ : ↑unitInterval) : (nelsen10 θ).IsSD

theorem Verification.nelsen10_isCD (θ : ↑unitInterval) : (nelsen10 θ).IsCD