← Copula mathematical handbook

The FGM density and its multivariate total positivity

def ProbabilityTheory.Copula.fgmDensity (θ : ℝ) (x : Fin 2 → ↑unitInterval) : ℝ

The Lebesgue density of a bivariate FGM copula.

Equations

• ProbabilityTheory.Copula.fgmDensity θ x = 1 + θ * (1 - 2 * ↑(x 0)) * (1 - 2 * ↑(x 1))

theorem ProbabilityTheory.Copula.continuous_fgmDensity (θ : ℝ) : Continuous (fgmDensity θ)

theorem ProbabilityTheory.Copula.fgmDensity_nonneg (θ : ℝ) (hθ : |θ| ≤ 1) (x : Fin 2 → ↑unitInterval) : 0 ≤ fgmDensity θ x

theorem ProbabilityTheory.Copula.integral_Iic_fgmDensity (θ : ℝ) (u : Fin 2 → ↑unitInterval) : ∫ (x : Fin 2 → ↑unitInterval) in Set.Iic u, fgmDensity θ x = fgmCDF θ (u 0) (u 1)

theorem ProbabilityTheory.Copula.toMeasure_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (fgmDensity θ x)

theorem ProbabilityTheory.Copula.isMTP2_fgmDensity_iff (θ : ℝ) : IsMTP2 (fgmDensity θ) ↔ 0 ≤ θ

theorem ProbabilityTheory.Copula.hasMTP2Density_fgm (θ : ℝ) (hθ : |θ| ≤ 1) (hpos : 0 ≤ θ) : (fgm θ hθ).HasMTP2Density