← Mathematical handbook

MTP2 of the positive-Clayton density formula

The measure equality needed for HasMTP2Density is proved in Copula.Dependence.ClaytonDensityMeasure.

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

The standard positive-Clayton density formula, set to zero on coordinate axes. Its identification as a density of the copula measure is proved in ClaytonDensityMeasure.

Equations

• ProbabilityTheory.Copula.claytonDensityFormula θ x = (1 + θ) * ↑(x 0) ^ (-θ - 1) * ↑(x 1) ^ (-θ - 1) * ProbabilityTheory.Copula.claytonKernel✝ θ (-2 - 1 / θ) (x 0) (x 1)

theorem ProbabilityTheory.Copula.isMTP2_claytonDensityFormula_positive (θ : ℝ) (hθ : 0 < θ) : IsMTP2 (claytonDensityFormula θ)

The explicit positive-Clayton density formula is MTP2 as a function. The corresponding copula-level theorem is in ClaytonDensityMeasure.

theorem ProbabilityTheory.Copula.claytonDensityFormula_nonneg (θ : ℝ) (hθ : 0 < θ) (x : Fin 2 → ↑unitInterval) : 0 ≤ claytonDensityFormula θ x

The explicit positive-Clayton density formula is nonnegative.

theorem ProbabilityTheory.Copula.measurable_claytonDensityFormula (θ : ℝ) : Measurable (claytonDensityFormula θ)

The explicit positive-Clayton density formula is measurable.