← Mathematical handbook

Symmetry identities for population concordance coefficients

theorem ProbabilityTheory.Copula.integral_reflect {d : ℕ} (C : Copula d) (s : Finset (Fin d)) (f : (Fin d → ↑unitInterval) → ℝ) (hf : Measurable f) : ∫ (x : Fin d → ↑unitInterval), f x ∂(C.reflect s).toMeasure = ∫ (x : Fin d → ↑unitInterval), f (reflectPoint s x) ∂C.toMeasure

theorem ProbabilityTheory.Copula.integral_transpose (C : Copula 2) (f : (Fin 2 → ↑unitInterval) → ℝ) (hf : Measurable f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂C.transpose.toMeasure = ∫ (x : Fin 2 → ↑unitInterval), f ![x 1, x 0] ∂C.toMeasure

@[simp]

theorem ProbabilityTheory.Copula.spearmanRho_transpose (C : Copula 2) : C.transpose.spearmanRho = C.spearmanRho

@[simp]

theorem ProbabilityTheory.Copula.kendallTau_transpose (C : Copula 2) : C.transpose.kendallTau = C.kendallTau

@[simp]

theorem ProbabilityTheory.Copula.spearmanFootrule_transpose (C : Copula 2) : C.transpose.spearmanFootrule = C.spearmanFootrule

@[simp]

theorem ProbabilityTheory.Copula.blomqvistBeta_transpose (C : Copula 2) : C.transpose.blomqvistBeta = C.blomqvistBeta

@[simp]

theorem ProbabilityTheory.Copula.giniGamma_transpose (C : Copula 2) : C.transpose.giniGamma = C.giniGamma

theorem ProbabilityTheory.Copula.spearmanRho_reflect_first (C : Copula 2) : (C.reflect {0}).spearmanRho = -C.spearmanRho

theorem ProbabilityTheory.Copula.kendallTau_reflect_first (C : Copula 2) : (C.reflect {0}).kendallTau = -C.kendallTau

theorem ProbabilityTheory.Copula.blomqvistBeta_reflect_first (C : Copula 2) : (C.reflect {0}).blomqvistBeta = -C.blomqvistBeta

theorem ProbabilityTheory.Copula.spearmanRho_reflect_second (C : Copula 2) : (C.reflect {1}).spearmanRho = -C.spearmanRho

theorem ProbabilityTheory.Copula.kendallTau_reflect_second (C : Copula 2) : (C.reflect {1}).kendallTau = -C.kendallTau

theorem ProbabilityTheory.Copula.blomqvistBeta_reflect_second (C : Copula 2) : (C.reflect {1}).blomqvistBeta = -C.blomqvistBeta

theorem ProbabilityTheory.Copula.giniGamma_reflect_first (C : Copula 2) : (C.reflect {0}).giniGamma = -C.giniGamma

theorem ProbabilityTheory.Copula.giniGamma_reflect_second (C : Copula 2) : (C.reflect {1}).giniGamma = -C.giniGamma

@[simp]

theorem ProbabilityTheory.Copula.spearmanRho_survivalCopula (C : Copula 2) : C.survivalCopula.spearmanRho = C.spearmanRho

@[simp]

theorem ProbabilityTheory.Copula.kendallTau_survivalCopula (C : Copula 2) : C.survivalCopula.kendallTau = C.kendallTau

@[simp]

theorem ProbabilityTheory.Copula.blomqvistBeta_survivalCopula (C : Copula 2) : C.survivalCopula.blomqvistBeta = C.blomqvistBeta

@[simp]

theorem ProbabilityTheory.Copula.giniGamma_survivalCopula (C : Copula 2) : C.survivalCopula.giniGamma = C.giniGamma

@[simp]

theorem ProbabilityTheory.Copula.spearmanFootrule_survivalCopula (C : Copula 2) : C.survivalCopula.spearmanFootrule = C.spearmanFootrule