← Copula mathematical handbook

Independence and the independence copula

Nelsen, An Introduction to Copulas, second edition, Theorem 2.4.2.

The coordinates of a random vector with law μ are independent exactly when μ is the product of its coordinate laws, μ = Measure.pi (marginal μ). This holds if and only if the independence copula Copula.independence d is a Sklar copula of μ. With continuous marginals the Sklar copula is unique, so independence is equivalent to the Sklar copula being Π.

theorem ProbabilityTheory.Copula.measureReal_Iic_pi {d : ℕ} (ν : Fin d → MeasureTheory.Measure ℝ) [∀ (i : Fin d), MeasureTheory.IsProbabilityMeasure (ν i)] (x : Fin d → ℝ) : (MeasureTheory.Measure.pi ν).real (Set.Iic x) = ∏ i : Fin d, (ν i).real (Set.Iic (x i))

The lower-orthant probability of a product measure is the product of the marginal CDF values.

theorem ProbabilityTheory.Copula.isSklarCopula_independence_of_eq_pi {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (hμ : ↑μ = MeasureTheory.Measure.pi fun (i : Fin d) => marginal μ i) : IsSklarCopula μ (independence d)

A law that is the product of its marginals has the independence copula as a Sklar copula.

theorem ProbabilityTheory.Copula.eq_pi_marginal_of_isSklarCopula_independence {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (h : IsSklarCopula μ (independence d)) : ↑μ = MeasureTheory.Measure.pi fun (i : Fin d) => marginal μ i

If the independence copula is a Sklar copula of a law, the law is the product of its marginals.

theorem ProbabilityTheory.Copula.isSklarCopula_independence_iff {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) : IsSklarCopula μ (independence d) ↔ ↑μ = MeasureTheory.Measure.pi fun (i : Fin d) => marginal μ i

Nelsen, Theorem 2.4.2. A law has the independence copula as a Sklar copula if and only if it is the product of its marginals.

theorem ProbabilityTheory.Copula.ofContinuousMarginals_eq_independence_iff {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) : ofContinuousMarginals μ hc = independence d ↔ ↑μ = MeasureTheory.Measure.pi fun (i : Fin d) => marginal μ i

With continuous marginals, the Sklar copula of a law is the independence copula if and only if the law is the product of its marginals.