← Copula mathematical handbook

Homogeneous Gaussian moments in polar coordinates

For a function h on ℝ² that is positively homogeneous of degree ν along rays, h(ρ cos θ, ρ sin θ) = ρ^ν g(θ), the integral against the standard bivariate Gaussian law splits into a radial moment and an angular integral:

E[h(Z₁, Z₂)] = R_ν ∫_{-π}^{π} g(θ) dθ, R_ν = ∫_0^∞ ρ^{ν+1} φ(ρ) φ(0) dρ > 0.

We apply this to the two moments that govern the tail dependence of the Student-t copula (Hult–Lindskog 2002): for (X, Y) ~ bivariateNormal r and a = arccos(r)/2,

• E[max(min(X, Y), 0)^ν] = 2 R_ν ∫_a^{π/2} cos^ν θ dθ,
• E[max(X, 0)^ν] = 2 R_ν ∫_0^{π/2} cos^ν θ dθ.

The first identity uses the symmetric representation (X, Y) = (c Z₁ − s Z₂, c Z₁ + s Z₂) with c = cos a, s = sin a (bivariateNormal_eq_map_symmetric), for which min(X, Y) = ρ cos(|θ| + a) in polar coordinates.

References

• H. Hult, F. Lindskog, Multivariate extremes, aggregation and dependence in elliptical distributions, Adv. Appl. Probab. 34 (2002).

noncomputable def ProbabilityTheory.Copula.gaussianRadialMoment (ν : ℝ) : ℝ

The radial moment R_ν = ∫_0^∞ ρ^{ν+1} φ(ρ) φ(0) dρ of the standard bivariate Gaussian law.

Equations

• ProbabilityTheory.Copula.gaussianRadialMoment ν = ∫ (ρ : ℝ) in Set.Ioi 0, ρ ^ (ν + 1) * (ProbabilityTheory.gaussianPDFReal 0 1 ρ * ProbabilityTheory.gaussianPDFReal 0 1 0)

theorem ProbabilityTheory.Copula.gaussianPDFReal_mul_gaussianPDFReal_zero (ρ : ℝ) : gaussianPDFReal 0 1 ρ * gaussianPDFReal 0 1 0 = (2 * Real.pi)⁻¹ * Real.exp (-(1 / 2) * ρ ^ 2)

The radial profile of the standard bivariate Gaussian density: φ(ρ) φ(0) = (2π)⁻¹ exp(−ρ²/2).

theorem ProbabilityTheory.Copula.gaussianRadialMoment_pos {ν : ℝ} (hν : -2 < ν) : 0 < gaussianRadialMoment ν

The radial moment is positive for ν > −2.

theorem ProbabilityTheory.Copula.integral_gaussianReal_prod_of_polar {ν : ℝ} (h : ℝ × ℝ → ℝ) (g : ℝ → ℝ) (hpolar : ∀ (ρ θ : ℝ), 0 < ρ → θ ∈ Set.Ioo (-Real.pi) Real.pi → h (ρ * Real.cos θ, ρ * Real.sin θ) = ρ ^ ν * g θ) : ∫ (p : ℝ × ℝ), h p ∂(gaussianReal 0 1).prod (gaussianReal 0 1) = gaussianRadialMoment ν * ∫ (θ : ℝ) in Set.Ioo (-Real.pi) Real.pi, g θ

Polar formula for homogeneous functions under the standard bivariate Gaussian law.

Angular integrals

theorem ProbabilityTheory.Copula.integral_Ioo_max_cos_abs_add_rpow {a ν : ℝ} (ha0 : 0 ≤ a) (ha : a ≤ Real.pi / 2) (hν : 0 < ν) : ∫ (θ : ℝ) in Set.Ioo (-Real.pi) Real.pi, max (Real.cos (|θ| + a)) 0 ^ ν = 2 * ∫ (θ : ℝ) in a..Real.pi / 2, Real.cos θ ^ ν

The angular integral ∫_{-π}^{π} max(cos(|θ| + a), 0)^ν dθ = 2 ∫_a^{π/2} cos^ν θ dθ.

The symmetric representation of the bivariate normal law

theorem ProbabilityTheory.Copula.bivariateNormal_eq_map_symmetric {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : bivariateNormal r = MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => (Real.cos (Real.arccos r / 2) * p.1 - Real.sin (Real.arccos r / 2) * p.2, Real.cos (Real.arccos r / 2) * p.1 + Real.sin (Real.arccos r / 2) * p.2)) ((gaussianReal 0 1).prod (gaussianReal 0 1))

For a = arccos(r)/2, (cos a Z₁ − sin a Z₂, cos a Z₁ + sin a Z₂) has the law bivariateNormal r.

The two tail moments

noncomputable def ProbabilityTheory.Copula.normalJointTailMoment (ν r : ℝ) : ℝ

The joint tail moment E[max(min(X, Y), 0)^ν] for (X, Y) ~ bivariateNormal r.

Equations

• ProbabilityTheory.Copula.normalJointTailMoment ν r = ∫ (p : ℝ × ℝ), max (min p.1 p.2) 0 ^ ν ∂ProbabilityTheory.Copula.bivariateNormal r

noncomputable def ProbabilityTheory.Copula.normalTailMoment (ν : ℝ) : ℝ

The marginal tail moment E[max(Z, 0)^ν] for Z ~ N(0, 1).

Equations

• ProbabilityTheory.Copula.normalTailMoment ν = ∫ (x : ℝ), max x 0 ^ ν ∂ProbabilityTheory.gaussianReal 0 1

theorem ProbabilityTheory.Copula.normalJointTailMoment_eq {ν r : ℝ} (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) : normalJointTailMoment ν r = gaussianRadialMoment ν * (2 * ∫ (θ : ℝ) in Real.arccos r / 2..Real.pi / 2, Real.cos θ ^ ν)

Polar form of the joint tail moment.

theorem ProbabilityTheory.Copula.normalTailMoment_eq {ν : ℝ} (hν : 0 < ν) : normalTailMoment ν = gaussianRadialMoment ν * (2 * ∫ (θ : ℝ) in 0..Real.pi / 2, Real.cos θ ^ ν)

Polar form of the marginal tail moment.

theorem ProbabilityTheory.Copula.bivariateNormal_map_fst {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map Prod.fst (bivariateNormal r) = gaussianReal 0 1

The first coordinate of bivariateNormal r is standard normal.

theorem ProbabilityTheory.Copula.integral_max_fst_rpow_bivariateNormal {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) : ∫ (p : ℝ × ℝ), max p.1 0 ^ ν ∂bivariateNormal r = normalTailMoment ν

The marginal tail moment computed under bivariateNormal r.

theorem ProbabilityTheory.Copula.integrable_abs_fst_rpow_bivariateNormal {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) {ν : ℝ} (hν : 0 < ν) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => |p.1| ^ ν) (bivariateNormal r)

|X|^ν is integrable under bivariateNormal r for ν ≥ 0.

theorem ProbabilityTheory.Copula.normalJointTailMoment_div_normalTailMoment {ν r : ℝ} (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) : normalJointTailMoment ν r / normalTailMoment ν = (∫ (θ : ℝ) in Real.arccos r / 2..Real.pi / 2, Real.cos θ ^ ν) / ∫ (θ : ℝ) in 0..Real.pi / 2, Real.cos θ ^ ν

The joint tail moment is the angular ratio times the marginal one.