← Copula mathematical handbook

Exact conditional moment profiles for the source diagonal bands

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.bandSquareLow (b v : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.bandSquareLow b v = √(2 * b * v) ^ 3 / (3 * b)

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.bandSquareHigh (b v : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.bandSquareHigh b v = 1 - 2 * v + ProbabilityTheory.Copula.RankRegion.XiRho.bandSquareLow b v

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.bandSquareMid (b v : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.bandSquareMid b v = if b ≤ 1 then v ^ 2 + b ^ 2 / 12 else v - 1 / (6 * b)

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.bandWeightLow (b v : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.bandWeightLow b v = v - √(2 * b * v) ^ 3 / (6 * b ^ 2)

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.bandWeightHigh (b v : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.bandWeightHigh b v = 1 / 2 - √(2 * b * v) ^ 3 / (6 * b ^ 2)

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.bandWeightMid (b v : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.bandWeightMid b v = if b ≤ 1 then v / 2 + b / 12 else v - v ^ 2 / 2 - 1 / (24 * b ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand_square_profile {b : ℝ} (hb : 0 < b) (v : ↑unitInterval) : Support.clampedSquare b (sourceBandIntercept b v) = if ↑v ≤ bandCut b then bandSquareLow b ↑v else if ↑v ≤ 1 - bandCut b then bandSquareMid b ↑v else bandSquareHigh b (1 - ↑v)

The complete second-moment profile, including both transition points.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand_weight_profile {b : ℝ} (hb : 0 < b) (v : ↑unitInterval) : Support.clampedWeight b (sourceBandIntercept b v) = if ↑v ≤ bandCut b then bandWeightLow b ↑v else if ↑v ≤ 1 - bandCut b then bandWeightMid b ↑v else bandWeightHigh b (1 - ↑v)

The complete weighted first-moment profile for Spearman rho.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand_xi_integral (b : ℝ) (hb : 0 < b) : (sourceBand b hb).chatterjeeXi = (6 * ∫ (v : ↑unitInterval), Support.clampedSquare b (sourceBandIntercept b v)) - 2

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand_rho_integral (b : ℝ) (hb : 0 < b) : (sourceBand b hb).spearmanRho = (12 * ∫ (v : ↑unitInterval), Support.clampedWeight b (sourceBandIntercept b v)) - 3