← Mathematical handbook

noncomputable def Verification.n17RealCDF (a u v : ℝ) : ℝ

Equations

• Verification.n17RealCDF a u v = (1 + ((1 + u) ^ a - 1) * ((1 + v) ^ a - 1) / Verification.n17A a) ^ a⁻¹ - 1

theorem Verification.n17RealCDF_eq (θ : ℝ) (hθ : θ ≠ 0) (u v : ↑unitInterval) : n17RealCDF (-θ) ↑u ↑v = (nelsen17 θ hθ).cdf ![u, v]

theorem Verification.n17RealCDF_deriv_zero {a : ℝ} (ha : a ≠ 0) (v : ℝ) : HasDerivAt (fun (u : ℝ) => n17RealCDF a u v) (n17Ratio a v) 0

theorem Verification.n17Ratio_ge_of_pqd (θ : ℝ) (hθ : θ ≠ 0) (hC : (nelsen17 θ hθ).IsPQD) (v : ↑unitInterval) : ↑v ≤ n17Ratio (-θ) ↑v

theorem Verification.n17Ratio_le_of_nqd (θ : ℝ) (hθ : θ ≠ 0) (hC : (nelsen17 θ hθ).IsNQD) (v : ↑unitInterval) : n17Ratio (-θ) ↑v ≤ ↑v

theorem Verification.n17Ratio_half_lt {a : ℝ} (ha : 1 < a) : n17Ratio a (1 / 2) < 1 / 2

theorem Verification.nelsen17_isCI_iff (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).IsCI ↔ -1 ≤ θ

theorem Verification.n17Ratio_half_gt {a : ℝ} (ha : a ≠ 0) (ha1 : a < 1) : 1 / 2 < n17Ratio a (1 / 2)

theorem Verification.nelsen17_isCD_iff (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).IsCD ↔ θ ≤ -1

theorem Verification.nelsen17_isPQD_iff (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).IsPQD ↔ -1 ≤ θ

theorem Verification.nelsen17_isNQD_iff (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).IsNQD ↔ θ ≤ -1