← Copula mathematical handbook

Orthant probabilities of the bivariate normal law (Sheppard's formula)

For a centered bivariate normal vector (X, Y) with equal variances and correlation r, P(X > 0, Y > 0) = P(X ≤ 0, Y ≤ 0) = 1/4 + arcsin r / (2π) (Sheppard 1899).

The bivariate normal law is described through its one-dimensional projections: we assume that aX + bY ~ N(0, (a² + 2abr + b²) v) for all real a, b. By the Cramér–Wold device (measure_prod_eq_of_map_linear_eq), this identifies the law of (X, Y) with that of (W₁, r W₁ + √(1 − r²) W₂) for independent W₁, W₂ ~ N(0, v). The probability of the corresponding wedge is computed in polar coordinates: the angle of (W₁, W₂) is uniform.

Main results

• measure_prod_eq_of_map_linear_eq: Cramér–Wold for finite measures on ℝ × ℝ.
• map_linear_prod_gaussianReal: aW₁ + bW₂ ~ N(0, a²v + b²w) for independent Gaussians.
• gaussianReal_prod_wedge: the wedge {0 < p₁, 0 < cos α p₁ + sin α p₂} has mass (π − α)/(2π).
• orthant_pos_of_linear_laws, orthant_nonpos_of_linear_laws: Sheppard's formula.

References

• W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation, Phil. Trans. R. Soc. A 192 (1899).
• W. H. Kruskal, Ordinal measures of association, J. Amer. Statist. Assoc. 53 (1958).

theorem ProbabilityTheory.Copula.measure_prod_eq_of_map_linear_eq {μ ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (a b : ℝ), MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => a * p.1 + b * p.2) μ = MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => a * p.1 + b * p.2) ν) : μ = ν

Cramér–Wold device on ℝ × ℝ: two finite measures with the same laws of all linear forms a p₁ + b p₂ coincide.

theorem ProbabilityTheory.Copula.gaussianReal_congr_var {m : ℝ} {v w : NNReal} (h : ↑v = ↑w) : gaussianReal m v = gaussianReal m w

Gaussian laws only depend on the real value of the variance.

theorem ProbabilityTheory.Copula.map_linear_prod_gaussianReal (v w : NNReal) (a b : ℝ) : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => a * p.1 + b * p.2) ((gaussianReal 0 v).prod (gaussianReal 0 w)) = gaussianReal 0 (a ^ 2 * ↑v + b ^ 2 * ↑w).toNNReal

A linear combination of two independent centered Gaussians is a centered Gaussian.

theorem ProbabilityTheory.Copula.gaussianReal_prod_eq_withDensity {v : NNReal} (hv : v ≠ 0) : (gaussianReal 0 v).prod (gaussianReal 0 v) = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => gaussianPDF 0 v p.1 * gaussianPDF 0 v p.2

The product of two copies of N(0, v) has the product Gaussian density.

theorem ProbabilityTheory.Copula.gaussianPDF_mul_polar (v : NNReal) (ρ θ : ℝ) : gaussianPDF 0 v (ρ * Real.cos θ) * gaussianPDF 0 v (ρ * Real.sin θ) = gaussianPDF 0 v ρ * gaussianPDF 0 v 0

The product Gaussian density is radial.

theorem ProbabilityTheory.Copula.gaussianReal_prod_cone {v : NNReal} (hv : v ≠ 0) (S : Set (ℝ × ℝ)) (A : Set ℝ) (hS : MeasurableSet S) (hA : MeasurableSet A) (hcone : ∀ (ρ θ : ℝ), 0 < ρ → θ ∈ Set.Ioo (-Real.pi) Real.pi → ((ρ * Real.cos θ, ρ * Real.sin θ) ∈ S ↔ θ ∈ A)) : ((gaussianReal 0 v).prod (gaussianReal 0 v)) S = (∫⁻ (ρ : ℝ) in Set.Ioi 0, ENNReal.ofReal ρ * (gaussianPDF 0 v ρ * gaussianPDF 0 v 0)) * MeasureTheory.volume (A ∩ Set.Ioo (-Real.pi) Real.pi)

Polar-coordinate formula for the mass of a cone under the product Gaussian law.

theorem ProbabilityTheory.Copula.wedge_angle_iff {α ρ θ : ℝ} (hα0 : 0 ≤ α) (hαπ : α ≤ Real.pi) (hρ : 0 < ρ) (hθ : θ ∈ Set.Ioo (-Real.pi) Real.pi) : 0 < ρ * Real.cos θ ∧ 0 < Real.cos α * (ρ * Real.cos θ) + Real.sin α * (ρ * Real.sin θ) ↔ θ ∈ Set.Ioo (α - Real.pi / 2) (Real.pi / 2)

The angular description of the wedge {0 < p₁, 0 < cos α p₁ + sin α p₂}.

theorem ProbabilityTheory.Copula.gaussianReal_prod_wedge {v : NNReal} (hv : v ≠ 0) {α : ℝ} (hα0 : 0 ≤ α) (hαπ : α ≤ Real.pi) : ((gaussianReal 0 v).prod (gaussianReal 0 v)) {p : ℝ × ℝ | 0 < p.1 ∧ 0 < Real.cos α * p.1 + Real.sin α * p.2} = ENNReal.ofReal ((Real.pi - α) / (2 * Real.pi))

The wedge between the directions 0 and α ∈ [0, π] (angle π − α) has Gaussian mass (π − α)/(2π).

theorem ProbabilityTheory.Copula.ae_ne_zero_of_map_eq_gaussianReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : Measurable X) {w : NNReal} (hw : w ≠ 0) (h : MeasureTheory.Measure.map X μ = gaussianReal 0 w) : ∀ᵐ (ω : Ω) ∂μ, X ω ≠ 0

A random variable with a nondegenerate centered Gaussian law is almost surely nonzero.

theorem ProbabilityTheory.Copula.orthant_pos_of_linear_laws {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {X Y : Ω → ℝ} (hX : Measurable X) (hY : Measurable Y) {r v : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hv : 0 < v) (hlaw : ∀ (a b : ℝ), MeasureTheory.Measure.map (fun (ω : Ω) => a * X ω + b * Y ω) μ = gaussianReal 0 ((a ^ 2 + 2 * a * b * r + b ^ 2) * v).toNNReal) : μ.real {ω : Ω | 0 < X ω ∧ 0 < Y ω} = 1 / 4 + Real.arcsin r / (2 * Real.pi)

Sheppard's formula (positive orthant). If every linear form aX + bY has law N(0, (a² + 2abr + b²) v) with v > 0, i.e. (X, Y) is centered bivariate normal with equal variances v and correlation r, then P(X > 0, Y > 0) = 1/4 + arcsin r / (2π).

theorem ProbabilityTheory.Copula.orthant_nonpos_of_linear_laws {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {X Y : Ω → ℝ} (hX : Measurable X) (hY : Measurable Y) {r v : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hv : 0 < v) (hlaw : ∀ (a b : ℝ), MeasureTheory.Measure.map (fun (ω : Ω) => a * X ω + b * Y ω) μ = gaussianReal 0 ((a ^ 2 + 2 * a * b * r + b ^ 2) * v).toNNReal) : μ.real {ω : Ω | X ω ≤ 0 ∧ Y ω ≤ 0} = 1 / 4 + Real.arcsin r / (2 * Real.pi)

Sheppard's formula (negative orthant): under the hypotheses of orthant_pos_of_linear_laws, P(X ≤ 0, Y ≤ 0) = 1/4 + arcsin r / (2π).