← Mathematical handbook

noncomputable def Verification.n18Psi (θ t : ℝ) : ℝ

Equations

• Verification.n18Psi θ t = Verification.n18Core θ (min t (Real.exp (-θ)))

noncomputable def Verification.n18Inv (θ : ℝ) (u : ↑unitInterval) : ℝ

Equations

• Verification.n18Inv θ u = if u = 1 then 0 else Real.exp (θ / (↑u - 1))

theorem Verification.n18Psi_convex {θ : ℝ} (hθ : 2 ≤ θ) : ConvexOn ℝ (Set.Ici 0) (n18Psi θ)

theorem Verification.n18Inv_nonneg (θ : ℝ) (u : ↑unitInterval) : 0 ≤ n18Inv θ u

theorem Verification.n18Inv_le_cutoff {θ : ℝ} (hθ : 0 < θ) (u : ↑unitInterval) : n18Inv θ u ≤ Real.exp (-θ)

theorem Verification.n18Inv_antitone {θ : ℝ} (hθ : 0 < θ) : Antitone (n18Inv θ)

noncomputable def Verification.n18Generator (θ : ℝ) (hθ : 2 ≤ θ) : ProbabilityTheory.Copula.BivariateGenerator

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Verification.nelsen18 (θ : ℝ) (hθ : 2 ≤ θ) : ProbabilityTheory.Copula 2

Equations

• Verification.nelsen18 θ hθ = (Verification.n18Generator θ hθ).copula

theorem Verification.nelsen18_cdf (θ : ℝ) (hθ : 2 ≤ θ) (u v : ↑unitInterval) : (nelsen18 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else n18Psi θ (n18Inv θ u + n18Inv θ v)

theorem Verification.n18Psi_eq_max {θ t : ℝ} (hθ : 0 < θ) (ht : 0 ≤ t) (ht1 : t < 1) : n18Psi θ t = max 0 (1 + θ / Real.log t)

theorem Verification.n18_sum_lt_one {θ : ℝ} (hθ : 2 ≤ θ) (u v : ↑unitInterval) : n18Inv θ u + n18Inv θ v < 1

theorem Verification.n18Inv_zero (θ : ℝ) : n18Inv θ 0 = Real.exp (-θ)

theorem Verification.nelsen18_cdf_full (θ : ℝ) (hθ : 2 ≤ θ) (u v : ↑unitInterval) : (nelsen18 θ hθ).cdf ![u, v] = max 0 (1 + θ / Real.log (n18Inv θ u + n18Inv θ v))

theorem Verification.nelsen18_cdf_of_lt_one (θ : ℝ) (hθ : 2 ≤ θ) (u v : ↑unitInterval) (hu : u < 1) (hv : v < 1) : (nelsen18 θ hθ).cdf ![u, v] = max 0 (1 + θ / Real.log (Real.exp (θ / (↑u - 1)) + Real.exp (θ / (↑v - 1))))