← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.gammaValue (s c m : ℝ) : ℝ

The explicit gamma coordinate in the source's boundary parametrization.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.rhoValue (s c q : ℝ) : ℝ

The explicit rho coordinate in the source's boundary parametrization.

Equations

• One or more equations did not get rendered due to their size.

inductive ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter : Type

• lowerEndpoint : UpperParameter
• upperEndpoint : UpperParameter
• halfShift (s : ℝ) (hs : 1 ≤ s) : UpperParameter
• right (S : RhoFootrule.RightData) : UpperParameter
• left (S : RhoFootrule.LeftData) : UpperParameter

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.gamma : UpperParameter → ℝ

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.lowerEndpoint.gamma = -1
• ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.upperEndpoint.gamma = 1
• (ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.halfShift s hs).gamma = ProbabilityTheory.Copula.RankRegion.RhoGamma.gammaValue s (3 / 8 - s / 2) (1 / 2)

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.rho : UpperParameter → ℝ

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.lowerEndpoint.rho = -1
• ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.upperEndpoint.rho = 1
• (ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.halfShift s hs).rho = ProbabilityTheory.Copula.RankRegion.RhoGamma.rhoValue s (3 / 8 - s / 2) (1 / 4)

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.copula : UpperParameter → Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.lowerEndpoint.copula = ProbabilityTheory.Copula.countermonotonic
• ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.upperEndpoint.copula = ProbabilityTheory.Copula.comonotonic 2
• (ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.halfShift s hs).copula = (ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift s hs).copula
• (ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.right S).copula = (ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.ofRight S).copula
• (ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.left S).copula = (ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.ofLeft S).copula

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.gamma_coefficient (p : UpperParameter) : p.copula.giniGamma = p.gamma

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.rho_coefficient (p : UpperParameter) : p.copula.spearmanRho = p.rho

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.maximizes (p : UpperParameter) (C : Copula 2) (h : C.giniGamma = p.gamma) : C.spearmanRho ≤ p.rho