← Mathematical handbook

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

The positive root gives the ratio of central and corner lengths.

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.splitRatio s c = (s + √(s ^ 2 + 2 * c)) / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.splitRatio_properties {s c w : ℝ} (hs : 0 < s) (hc : c < 0) (_hw : 0 ≤ w) (hdisc : w ^ 2 ≤ s ^ 2 + 2 * c) : 0 < splitRatio s c ∧ splitRatio s c < s ∧ s + w ≤ 2 * splitRatio s c ∧ 2 * splitRatio s c * (splitRatio s c - s) = c

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

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.centralLength s c = ProbabilityTheory.Copula.RankRegion.RhoGamma.splitRatio s c / (1 + ProbabilityTheory.Copula.RankRegion.RhoGamma.splitRatio s c)

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

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.cornerLength s c = 1 / (1 + ProbabilityTheory.Copula.RankRegion.RhoGamma.splitRatio s c)

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

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.supportingSlope s c = s * ProbabilityTheory.Copula.RankRegion.RhoGamma.cornerLength s c

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.splitting_properties {s c w : ℝ} (hs : 0 < s) (hc : c < 0) (hw : 0 ≤ w) (hdisc : w ^ 2 ≤ s ^ 2 + 2 * c) : 0 < centralLength s c ∧ centralLength s c < 1 ∧ 0 < cornerLength s c ∧ centralLength s c + cornerLength s c = 1 ∧ centralLength s c < supportingSlope s c ∧ supportingSlope s c + cornerLength s c * w ≤ 2 * centralLength s c ∧ cornerLength s c ^ 2 * c = 2 * centralLength s c * (centralLength s c - supportingSlope s c)