← Copula mathematical handbook

The positive-parameter Clayton construction

Take independent rate-one exponentials E i and an independent gamma variable G with shape 1/θ and rate one. The joint law of -E i / G has atomless marginals; its unique Sklar copula is the gamma-frailty construction of Clayton. This module supplies the stochastic construction and its Sklar factorization. Copula.Families.Clayton.CDF identifies the closed-form Archimedean CDF, and Copula.Families.Clayton.Limits proves its two endpoint limits.

noncomputable def ProbabilityTheory.Copula.claytonFrailtySource (d : ℕ) (θ : ℝ) (hθ : 0 < θ) : MeasureTheory.ProbabilityMeasure ((Fin d → ℝ) × ℝ)

Independent exponential numerators and their common gamma frailty.

Equations

• ProbabilityTheory.Copula.claytonFrailtySource d θ hθ = ⟨(MeasureTheory.Measure.pi fun (x : Fin d) => ProbabilityTheory.expMeasure 1).prod (ProbabilityTheory.gammaMeasure θ⁻¹ 1), ⋯⟩

noncomputable def ProbabilityTheory.Copula.claytonLaw (d : ℕ) (θ : ℝ) (hθ : 0 < θ) : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)

The joint negative exponential/gamma ratios used in the Clayton construction.

Equations

• ProbabilityTheory.Copula.claytonLaw d θ hθ = (ProbabilityTheory.Copula.claytonFrailtySource d θ hθ).map fun (p : (Fin d → ℝ) × ℝ) (i : Fin d) => -(p.1 i / p.2)

theorem ProbabilityTheory.Copula.atomless_claytonLaw_marginal (d : ℕ) (θ : ℝ) (hθ : 0 < θ) (i : Fin d) : MeasureTheory.NullSingletonClass (marginal (claytonLaw d θ hθ) i)

theorem ProbabilityTheory.Copula.continuous_claytonLaw_marginal (d : ℕ) (θ : ℝ) (hθ : 0 < θ) (i : Fin d) : Continuous ↑(ProbabilityTheory.cdf (marginal (claytonLaw d θ hθ) i))

noncomputable def ProbabilityTheory.Copula.clayton (d : ℕ) (θ : ℝ) (hθ : 0 < θ) : Copula d

The positive-parameter Clayton copula, constructed from gamma frailty.

Equations

• ProbabilityTheory.Copula.clayton d θ hθ = ProbabilityTheory.Copula.ofContinuousMarginals (ProbabilityTheory.Copula.claytonLaw d θ hθ) ⋯

theorem ProbabilityTheory.Copula.isSklarCopula_clayton (d : ℕ) (θ : ℝ) (hθ : 0 < θ) : IsSklarCopula (claytonLaw d θ hθ) (clayton d θ hθ)