← Mathematical handbook

Lower-orthant parameter order of the Genest–Ghoudi family (Nelsen 15)

With φ_c(t)=(1-t^{1/c})^c and ψ_c(x)=((1-x^{1/c})₊)^c, the copula is ψ_c(φ_c(u)+φ_c(v)). For θ≤η the generator ratio φ_θ/φ_η is nondecreasing on (0,1) (its logarithmic derivative is z/(1-z) evaluated at two ordered powers of t), and φ_η ≤ φ_θ. The classical ratio argument (Nelsen, Corollary 4.4.6) then gives C_θ ≤ C_η pointwise.

noncomputable def Verification.GenestGhoudiOrder.phi (c t : ℝ) : ℝ

The generator φ_c(t)=(1-t^{1/c})^c.

Equations

• Verification.GenestGhoudiOrder.phi c t = (1 - t ^ c⁻¹) ^ c

noncomputable def Verification.GenestGhoudiOrder.psi (c x : ℝ) : ℝ

The inverse generator ψ_c(x)=((1-x^{1/c})₊)^c.

Equations

• Verification.GenestGhoudiOrder.psi c x = max 0 (1 - x ^ c⁻¹) ^ c

theorem Verification.GenestGhoudiOrder.one_sub_rpow_nonneg {c : ℝ} (hc : 1 ≤ c) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : 0 ≤ 1 - t ^ c⁻¹

theorem Verification.GenestGhoudiOrder.phi_nonneg {c : ℝ} (hc : 1 ≤ c) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : 0 ≤ phi c t

theorem Verification.GenestGhoudiOrder.phi_one {c : ℝ} (hc : 1 ≤ c) : phi c 1 = 0

theorem Verification.GenestGhoudiOrder.psi_phi {c : ℝ} (hc : 1 ≤ c) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : psi c (phi c t) = t

theorem Verification.GenestGhoudiOrder.phi_psi {c : ℝ} (hc : 1 ≤ c) {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : phi c (psi c x) = x

theorem Verification.GenestGhoudiOrder.psi_antitone {c : ℝ} (hc : 1 ≤ c) {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) : psi c y ≤ psi c x

theorem Verification.GenestGhoudiOrder.psi_nonneg {c : ℝ} (_hc : 1 ≤ c) (x : ℝ) : 0 ≤ psi c x

theorem Verification.GenestGhoudiOrder.psi_of_one_le {c : ℝ} (hc : 1 ≤ c) {x : ℝ} (hx : 1 ≤ x) : psi c x = 0

theorem Verification.GenestGhoudiOrder.psi_le_one {c : ℝ} (hc : 1 ≤ c) {x : ℝ} (hx : 0 ≤ x) : psi c x ≤ 1

theorem Verification.GenestGhoudiOrder.phi_le_phi {θ η : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : phi η t ≤ phi θ t

φ_η ≤ φ_θ for θ≤η.

noncomputable def Verification.GenestGhoudiOrder.logRatio (θ η t : ℝ) : ℝ

The logarithmic generator ratio.

Equations

• Verification.GenestGhoudiOrder.logRatio θ η t = θ * Real.log (1 - t ^ θ⁻¹) - η * Real.log (1 - t ^ η⁻¹)

theorem Verification.GenestGhoudiOrder.hasDerivAt_logTerm {c : ℝ} (hc : 1 ≤ c) {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) : HasDerivAt (fun (x : ℝ) => c * Real.log (1 - x ^ c⁻¹)) (-(t ^ c⁻¹ / t) / (1 - t ^ c⁻¹)) t

theorem Verification.GenestGhoudiOrder.logRatio_monotoneOn {θ η : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) : MonotoneOn (logRatio θ η) (Set.Ioo 0 1)

theorem Verification.GenestGhoudiOrder.phi_ratio {θ η : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) (ht : t ≤ 1) : phi θ s * phi η t ≤ phi θ t * phi η s

The generator ratio φ_θ/φ_η is nondecreasing, in cross-multiplied form.

theorem Verification.GenestGhoudiOrder.cdf_eq_psi (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) : (ProbabilityTheory.Copula.genestGhoudi θ hθ).cdf ![u, v] = psi θ (phi θ ↑u + phi θ ↑v)

The Genest–Ghoudi CDF in generator form.

theorem Verification.GenestGhoudiOrder.genestGhoudi_cdf_mono {θ η : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.genestGhoudi θ hθ).cdf ![u, v] ≤ (ProbabilityTheory.Copula.genestGhoudi η ⋯).cdf ![u, v]

Table 3: Genest–Ghoudi increases in lower-orthant order.

theorem Verification.GenestGhoudiOrder.genestGhoudi_lowerOrthant_mono {θ η : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) : (ProbabilityTheory.Copula.genestGhoudi θ hθ).LowerOrthantLE (ProbabilityTheory.Copula.genestGhoudi η ⋯)