← Mathematical handbook

The bivariate Farlie–Gumbel–Morgenstern family

def ProbabilityTheory.Copula.fgmCDF (θ : ℝ) (u v : ↑unitInterval) : ℝ

The FGM polynomial, including its boundary values.

Equations

• ProbabilityTheory.Copula.fgmCDF θ u v = ↑u * ↑v * (1 + θ * (1 - ↑u) * (1 - ↑v))

theorem ProbabilityTheory.Copula.isClassical_fgmCDF (θ : ℝ) (hθ : |θ| ≤ 1) : IsClassical fun (u : Fin 2 → ↑unitInterval) => fgmCDF θ (u 0) (u 1)

noncomputable def ProbabilityTheory.Copula.fgm (θ : ℝ) (hθ : |θ| ≤ 1) : Copula 2

FGM copulas for the full parameter interval [-1,1].

Equations

• ProbabilityTheory.Copula.fgm θ hθ = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => ProbabilityTheory.Copula.fgmCDF θ (u 0) (u 1)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_fgm (θ : ℝ) (hθ : |θ| ≤ 1) (u : Fin 2 → ↑unitInterval) : (fgm θ hθ).cdf u = fgmCDF θ (u 0) (u 1)

@[simp]

theorem ProbabilityTheory.Copula.fgm_zero : fgm 0 ⋯ = independence 2