← Copula mathematical handbook

Copulas with quadratic sections

A bivariate copula has quadratic sections in u if every vertical section u ↦ C(u, v) is a polynomial of degree at most two (Nelsen, An Introduction to Copulas, 2nd ed., §3.2.5). The boundary conditions force the form

C(u, v) = u v + ψ(v) u (1 - u),

and this function is a copula if and only if ψ(0) = ψ(1) = 0 and ψ is 1-Lipschitz (IsQuadraticSectionFunction).

Main results:

• quadraticSectionCopula ψ hψ with cdf_quadraticSectionCopula;
• exists_copula_quadraticSection_iff: the formula u v + ψ(v) u (1 - u) is the CDF of a copula if and only if ψ satisfies the two conditions (both directions);
• eq_quadraticSectionCopula_of_quadratic: a copula whose vertical sections are quadratic polynomials a(v) u² + b(v) u + c(v) is quadraticSectionCopula (-a);
• quadraticSectionCopula_eq_fgm_of_transpose, quadratic_sections_both_iff_fgm: a copula has quadratic sections in both u and v if and only if it is a Farlie–Gumbel–Morgenstern copula.

structure ProbabilityTheory.Copula.IsQuadraticSectionFunction (ψ : ↑unitInterval → ℝ) : Prop

The admissibility conditions for the coefficient function of a copula with quadratic sections in u: ψ(0) = ψ(1) = 0 and ψ is 1-Lipschitz.

• zero : ψ 0 = 0

  Vanishing at zero.

• one : ψ 1 = 0

  Vanishing at one.

• lipschitz (s t : ↑unitInterval) : |ψ t - ψ s| ≤ |↑t - ↑s|

  The Lipschitz condition.

def ProbabilityTheory.Copula.quadraticSectionCDF (ψ : ↑unitInterval → ℝ) (u v : ↑unitInterval) : ℝ

The function u v + ψ(v) u (1 - u).

Equations

• ProbabilityTheory.Copula.quadraticSectionCDF ψ u v = ↑u * ↑v + ψ v * (↑u * (1 - ↑u))

theorem ProbabilityTheory.Copula.IsQuadraticSectionFunction.isClassical {ψ : ↑unitInterval → ℝ} (hψ : IsQuadraticSectionFunction ψ) : IsClassical fun (u : Fin 2 → ↑unitInterval) => quadraticSectionCDF ψ (u 0) (u 1)

noncomputable def ProbabilityTheory.Copula.quadraticSectionCopula (ψ : ↑unitInterval → ℝ) (hψ : IsQuadraticSectionFunction ψ) : Copula 2

The copula u v + ψ(v) u (1 - u) with quadratic sections in u.

Equations

• ProbabilityTheory.Copula.quadraticSectionCopula ψ hψ = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => ProbabilityTheory.Copula.quadraticSectionCDF ψ (u 0) (u 1)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_quadraticSectionCopula (ψ : ↑unitInterval → ℝ) (hψ : IsQuadraticSectionFunction ψ) (u : Fin 2 → ↑unitInterval) : (quadraticSectionCopula ψ hψ).cdf u = quadraticSectionCDF ψ (u 0) (u 1)

theorem ProbabilityTheory.Copula.cdf_quadraticSectionCopula_two (ψ : ↑unitInterval → ℝ) (hψ : IsQuadraticSectionFunction ψ) (u v : ↑unitInterval) : (quadraticSectionCopula ψ hψ).cdf ![u, v] = quadraticSectionCDF ψ u v

theorem ProbabilityTheory.Copula.cdf_rectangle_nonneg (C : Copula 2) {a b c e : ↑unitInterval} (hab : a ≤ b) (hce : c ≤ e) : 0 ≤ C.cdf ![b, e] - C.cdf ![a, e] - C.cdf ![b, c] + C.cdf ![a, c]

Nonnegative bivariate rectangle increments of a copula CDF.

theorem ProbabilityTheory.Copula.exists_copula_quadraticSection_iff (ψ : ↑unitInterval → ℝ) : (∃ (C : Copula 2), ∀ (u v : ↑unitInterval), C.cdf ![u, v] = quadraticSectionCDF ψ u v) ↔ IsQuadraticSectionFunction ψ

Nelsen §3.2.5: characterization of copulas with quadratic sections. The function u v + ψ(v) u (1 - u) is the CDF of a copula if and only if ψ(0) = ψ(1) = 0 and |ψ(t) - ψ(s)| ≤ |t - s|.

theorem ProbabilityTheory.Copula.eq_quadraticSectionCopula_of_quadratic (C : Copula 2) (a b c : ↑unitInterval → ℝ) (h : ∀ (u v : ↑unitInterval), C.cdf ![u, v] = a v * ↑u ^ 2 + b v * ↑u + c v) : ∃ (hψ : IsQuadraticSectionFunction fun (v : ↑unitInterval) => -a v), C = quadraticSectionCopula (fun (v : ↑unitInterval) => -a v) hψ

Copulas with quadratic sections in u (Nelsen §3.2.5): if every vertical section of C is a quadratic polynomial u ↦ a(v) u² + b(v) u + c(v), then C(u,v) = u v + ψ(v) u (1 - u) with ψ = -a, and ψ satisfies the admissibility conditions.

theorem ProbabilityTheory.Copula.fgmCDF_eq_quadraticSectionCDF (θ : ℝ) (u v : ↑unitInterval) : fgmCDF θ u v = quadraticSectionCDF (fun (v : ↑unitInterval) => θ * (↑v * (1 - ↑v))) u v

The FGM copula has quadratic sections, with ψ(v) = θ v (1 - v).

theorem ProbabilityTheory.Copula.quadraticSectionCopula_eq_fgm {ψ φ : ↑unitInterval → ℝ} (hψ : IsQuadraticSectionFunction ψ) (h : ∀ (u v : ↑unitInterval), quadraticSectionCDF ψ u v = ↑u * ↑v + φ u * (↑v * (1 - ↑v))) : ∃ (hθ : |4 * φ unitHalf| ≤ 1), quadraticSectionCopula ψ hψ = fgm (4 * φ unitHalf) hθ

Quadratic sections in both variables force the FGM family (Nelsen §3.2.5): if the copula u v + ψ(v) u (1 - u) also equals u v + φ(u) v (1 - v) for some φ, then it is the FGM copula with parameter θ = 4 φ(1/2) and |θ| ≤ 1.

theorem ProbabilityTheory.Copula.quadratic_sections_both_iff_fgm (C : Copula 2) : ((∃ (ψ : ↑unitInterval → ℝ), ∀ (u v : ↑unitInterval), C.cdf ![u, v] = quadraticSectionCDF ψ u v) ∧ ∃ (φ : ↑unitInterval → ℝ), ∀ (u v : ↑unitInterval), C.cdf ![u, v] = ↑u * ↑v + φ u * (↑v * (1 - ↑v))) ↔ ∃ (θ : ℝ) (hθ : |θ| ≤ 1), C = fgm θ hθ

A copula has quadratic sections in both u and v iff it is an FGM copula (Nelsen §3.2.5).