Documentation

Copula.Reflection.Bivariate

← Mathematical handbook

Bivariate reflections and survival copulas #

theorem ProbabilityTheory.Copula.ext_cdf_two {C D : Copula 2} (h : ∀ (u v : ↑unitInterval), C.cdf ![u, v] = D.cdf ![u, v]) :

C = D

noncomputable def ProbabilityTheory.Copula.transpose (C : Copula 2) :

Transposition exchanges the two coordinates.

Equations

C.transpose = C.reindex ![1, 0]

Instances For

noncomputable def ProbabilityTheory.Copula.survivalCopula {d : ℕ} (C : Copula d) :

The survival copula, obtained by reflecting every coordinate.

Equations

C.survivalCopula = C.reflect Finset.univ

Instances For

@[simp]

theorem ProbabilityTheory.Copula.transpose_transpose (C : Copula 2) :

C.transpose.transpose = C

@[simp]

theorem ProbabilityTheory.Copula.survivalCopula_survivalCopula {d : ℕ} (C : Copula d) :

C.survivalCopula.survivalCopula = C

@[simp]

theorem ProbabilityTheory.Copula.cdf_transpose (C : Copula 2) (u v : ↑unitInterval) :

C.transpose.cdf ![u, v] = C.cdf ![v, u]

theorem ProbabilityTheory.Copula.cdf_survivalCopula (C : Copula 2) (u v : ↑unitInterval) :

C.survivalCopula.cdf ![u, v] = ↑u + ↑v - 1 + C.cdf ![unitInterval.symm u, unitInterval.symm v]

The usual bivariate survival-copula formula.

theorem ProbabilityTheory.Copula.cdf_reflect_first (C : Copula 2) (u v : ↑unitInterval) :

(C.reflect {0}).cdf ![u, v] = ↑v - C.cdf ![unitInterval.symm u, v]

theorem ProbabilityTheory.Copula.transpose_reflect_first (C : Copula 2) :

(C.reflect {0}).transpose = C.transpose.reflect {1}

theorem ProbabilityTheory.Copula.cdf_reflect_second (C : Copula 2) (u v : ↑unitInterval) :

(C.reflect {1}).cdf ![u, v] = ↑u - C.cdf ![u, unitInterval.symm v]

theorem ProbabilityTheory.Copula.reflect_first_second (C : Copula 2) :

(C.reflect {0}).reflect {1} = C.survivalCopula