← Copula mathematical handbook

Differentiable Archimedean generators and conditional distributions

For the analytic formulas of Nelsen, An Introduction to Copulas, second edition, Theorem 4.3.4 (the Kendall distribution function) and Corollary 5.1.4 (Kendall's tau via the generator), we consider generators whose inverse generator ψ has a continuous derivative ψ' on its positivity region {s > 0 : ψ(s) > 0} (BivariateGenerator.IsC1; for strict generators this is (0, ∞), see BivariateGenerator.IsC1.of_isStrict). Then:

• the generator φ is continuous on (0, 1) for every generator (BivariateGenerator.continuousAt_invFunReal);
• ψ' < 0 where ψ > 0 (BivariateGenerator.IsC1.deriv_neg) and φ'(u) = 1 / ψ'(φ(u)) on (0, 1) (BivariateGenerator.IsC1.hasDerivAt_invFunReal);
• the first partial derivative is ∂₁C(u, v) = ψ'(φ(u) + φ(v)) / ψ'(φ(u)) where C(u, v) > 0 (BivariateGenerator.IsC1.hasDerivAt_cdfSection);
• for almost every u, the conditional distribution function of the second coordinate given the first equals this partial derivative simultaneously for all v > 0 with C(u, v) > 0 (BivariateGenerator.IsC1.ae_conditionalCDF_eq). The exceptional null set is chosen once, via rational thresholds, monotonicity of the conditional CDF and continuity of the partial derivative in v.

theorem ProbabilityTheory.Copula.BivariateGenerator.continuousAt_invFunReal (g : BivariateGenerator) {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : ContinuousAt g.invFunReal x

The generator is continuous on (0, 1).

structure ProbabilityTheory.Copula.BivariateGenerator.IsC1 (g : BivariateGenerator) (ψ' : ℝ → ℝ) : Prop

A generator whose inverse generator ψ is continuously differentiable, with derivative ψ', on its positivity region {s > 0 : ψ(s) > 0} (all of (0, ∞) for a strict generator, (0, φ(0)) for a non-strict one). The values of ψ' elsewhere are not used.

• hasDerivAt (s : ℝ) : 0 < s → 0 < g.toFun s → HasDerivAt g.toFun (ψ' s) s

  ψ' is the derivative of ψ where ψ is positive.

• continuousAt (s : ℝ) : 0 < s → 0 < g.toFun s → ContinuousAt ψ' s

  The derivative is continuous where ψ is positive.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.of_isStrict {g : BivariateGenerator} {ψ' : ℝ → ℝ} (hd : ∀ (s : ℝ), 0 < s → HasDerivAt g.toFun (ψ' s) s) (hc : ContinuousOn ψ' (Set.Ioi 0)) : g.IsC1 ψ'

A strict generator with ψ continuously differentiable on (0, ∞).

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.deriv_neg {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') {s : ℝ} (hs : 0 < s) (hpos : 0 < g.toFun s) : ψ' s < 0

The derivative of an inverse generator is negative where the inverse generator is positive.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.deriv_ne_zero {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') {s : ℝ} (hs : 0 < s) (hpos : 0 < g.toFun s) : ψ' s ≠ 0

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.invFunReal_pos {g : BivariateGenerator} {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : 0 < g.invFunReal x

The generator is positive on (0, 1), as a real function.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.toFun_invFunReal {g : BivariateGenerator} {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : g.toFun (g.invFunReal x) = x

ψ(φ(x)) = x for x ∈ (0, 1], for the real extension of the generator.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.hasDerivAt_invFunReal {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : HasDerivAt g.invFunReal (ψ' (g.invFunReal x))⁻¹ x

φ'(x) = 1 / ψ'(φ(x)) on (0, 1).

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.cdfSection_eq (g : BivariateGenerator) {v : ↑unitInterval} (hv : v ≠ 0) {y : ℝ} (hy : y ∈ Set.Ioo 0 1) : g.copula.cdfSection v y = g.toFun (g.invFunReal y + g.invFun v)

The CDF section of the copula of a generator, at an interior first coordinate.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.hasDerivAt_cdfSection {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') {x : ℝ} (hx : x ∈ Set.Ioo 0 1) {v : ↑unitInterval} (hv : v ≠ 0) (hC : 0 < g.toFun (g.invFunReal x + g.invFun v)) : HasDerivAt (g.copula.cdfSection v) (ψ' (g.invFunReal x + g.invFun v) * (ψ' (g.invFunReal x))⁻¹) x

The first partial derivative ∂₁C(x, v) = ψ'(φ(x) + φ(v)) / ψ'(φ(x)) at x ∈ (0, 1) with C(x, v) > 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.conditionalCDF_mono (C : Copula 2) (u : ↑unitInterval) {v w : ↑unitInterval} (hvw : v ≤ w) : C.conditionalCDF u v ≤ C.conditionalCDF u w

The conditional CDF is monotone in the threshold.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.conditionalCDF_one (C : Copula 2) (u : ↑unitInterval) : C.conditionalCDF u 1 = 1

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.ae_conditionalCDF_eq {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') : ∀ᵐ (u : ↑unitInterval), u ≠ 0 ∧ u ≠ 1 ∧ ∀ (v : ↑unitInterval), v ≠ 0 → 0 < g.toFun (g.invFun u + g.invFun v) → g.copula.conditionalCDF u v = ψ' (g.invFun u + g.invFun v) * (ψ' (g.invFun u))⁻¹

For almost every u, the conditional distribution function of the copula of a C¹ generator is the partial derivative ψ'(φ(u) + φ(v)) / ψ'(φ(u)), simultaneously for all thresholds v > 0 with C(u, v) > 0.