← Copula mathematical handbook

Product perturbations of independence

For Lipschitz functions φ ψ : I → ℝ vanishing at both endpoints, with Lipschitz constants Lφ and Lψ satisfying Lφ * Lψ ≤ 1, the function

C(u,v) = uv + φ(u) ψ(v)

is a copula: its rectangle increments are (b-a)(e-c) + (φ b - φ a)(ψ e - ψ c), which are bounded below by (1 - Lφ Lψ)(b-a)(e-c) ≥ 0. This covers the tent copulas Π ± ℓ ⊗ τ, the Blomqvist copulas Π + b ℓ ⊗ ℓ, and the sine copulas Π + (a/π) sin(π ·) ⊗ ℓ.

structure ProbabilityTheory.Copula.BoundaryProfile : Type

A real function on the unit interval that vanishes at both endpoints and is Lipschitz with constant lip.

• toFun : ↑unitInterval → ℝ

  The profile function.

• lip : ℝ

  Its Lipschitz constant.

• lip_nonneg : 0 ≤ self.lip
• zero : self.toFun 0 = 0
• one : self.toFun 1 = 0
• lipschitz (s t : ↑unitInterval) : |self.toFun s - self.toFun t| ≤ self.lip * |↑s - ↑t|

@[instance_reducible]

instance ProbabilityTheory.Copula.BoundaryProfile.instCoeFunForallElemRealUnitInterval : CoeFun BoundaryProfile fun (x : BoundaryProfile) => ↑unitInterval → ℝ

Equations

• ProbabilityTheory.Copula.BoundaryProfile.instCoeFunForallElemRealUnitInterval = { coe := ProbabilityTheory.Copula.BoundaryProfile.toFun }

theorem ProbabilityTheory.Copula.BoundaryProfile.abs_le (φ : BoundaryProfile) (t : ↑unitInterval) : |φ.toFun t| ≤ φ.lip * min (↑t) (1 - ↑t)

noncomputable def ProbabilityTheory.Copula.BoundaryProfile.smul (c : ℝ) (φ : BoundaryProfile) : BoundaryProfile

The scaled profile c • φ.

Equations

• ProbabilityTheory.Copula.BoundaryProfile.smul c φ = { toFun := fun (t : ↑unitInterval) => c * φ.toFun t, lip := |c| * φ.lip, lip_nonneg := ⋯, zero := ⋯, one := ⋯, lipschitz := ⋯ }

@[simp]

theorem ProbabilityTheory.Copula.BoundaryProfile.smul_apply (c : ℝ) (φ : BoundaryProfile) (t : ↑unitInterval) : (smul c φ).toFun t = c * φ.toFun t

noncomputable def ProbabilityTheory.Copula.productPerturbationCDF (φ ψ : BoundaryProfile) (u v : ↑unitInterval) : ℝ

The bivariate function uv + φ(u) ψ(v).

Equations

• ProbabilityTheory.Copula.productPerturbationCDF φ ψ u v = ↑u * ↑v + φ.toFun u * ψ.toFun v

theorem ProbabilityTheory.Copula.productPerturbation_isClassical (φ ψ : BoundaryProfile) (h : φ.lip * ψ.lip ≤ 1) : IsClassical fun (u : Fin 2 → ↑unitInterval) => productPerturbationCDF φ ψ (u 0) (u 1)

noncomputable def ProbabilityTheory.Copula.productPerturbation (φ ψ : BoundaryProfile) (h : φ.lip * ψ.lip ≤ 1) : Copula 2

The copula Π + φ ⊗ ψ for boundary profiles with Lip φ * Lip ψ ≤ 1.

Equations

• ProbabilityTheory.Copula.productPerturbation φ ψ h = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => ProbabilityTheory.Copula.productPerturbationCDF φ ψ (u 0) (u 1)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_productPerturbation (φ ψ : BoundaryProfile) (h : φ.lip * ψ.lip ≤ 1) (u v : ↑unitInterval) : (productPerturbation φ ψ h).cdf ![u, v] = ↑u * ↑v + φ.toFun u * ψ.toFun v