← Copula mathematical handbook

The independence copula

The independence copula is the product of the uniform probability measures. Its CDF is the product of the coordinates, including the empty product in dimension zero.

noncomputable def ProbabilityTheory.Copula.independence (d : ℕ) : Copula d

The independence (product) copula.

Equations

• ProbabilityTheory.Copula.independence d = { measure := ⟨MeasureTheory.Measure.pi fun (x : Fin d) => MeasureTheory.volume, ⋯⟩, marginal_eq := ⋯ }

@[simp]

theorem ProbabilityTheory.Copula.toMeasure_independence (d : ℕ) : (independence d).toMeasure = MeasureTheory.Measure.pi fun (x : Fin d) => MeasureTheory.volume

@[instance_reducible]

noncomputable instance ProbabilityTheory.Copula.instInhabited (d : ℕ) : Inhabited (Copula d)

Equations

• ProbabilityTheory.Copula.instInhabited d = { default := ProbabilityTheory.Copula.independence d }

@[simp]

theorem ProbabilityTheory.Copula.cdf_independence {d : ℕ} (u : Fin d → ↑unitInterval) : (independence d).cdf u = ∏ i : Fin d, ↑(u i)