← Copula mathematical handbook

Exact integrals of the diagonal-band moment profiles

theorem ProbabilityTheory.Copula.RankRegion.XiRho.bandSquare_pair_integral (b c : ℝ) : ∫ (v : ℝ) in 0..c, bandSquareLow b v + bandSquareHigh b v = c - c ^ 2 + 2 / (3 * b) * ∫ (v : ℝ) in 0..c, √(2 * b * v) ^ 3

theorem ProbabilityTheory.Copula.RankRegion.XiRho.bandWeight_pair_integral (b c : ℝ) : ∫ (v : ℝ) in 0..c, bandWeightLow b v + bandWeightHigh b v = c / 2 + c ^ 2 / 2 - 1 / (3 * b ^ 2) * ∫ (v : ℝ) in 0..c, √(2 * b * v) ^ 3

theorem ProbabilityTheory.Copula.RankRegion.XiRho.bandSquare_mid_small (b c d : ℝ) (hb : b ≤ 1) : ∫ (v : ℝ) in c..d, bandSquareMid b v = (d ^ 3 - c ^ 3) / 3 + b ^ 2 / 12 * (d - c)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.bandSquare_mid_large (b c d : ℝ) (hb : ¬b ≤ 1) : ∫ (v : ℝ) in c..d, bandSquareMid b v = (d ^ 2 - c ^ 2) / 2 - (d - c) / (6 * b)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.bandWeight_mid_small (b c d : ℝ) (hb : b ≤ 1) : ∫ (v : ℝ) in c..d, bandWeightMid b v = (d ^ 2 - c ^ 2) / 4 + b / 12 * (d - c)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.bandWeight_mid_large (b c d : ℝ) (hb : ¬b ≤ 1) : ∫ (v : ℝ) in c..d, bandWeightMid b v = (d ^ 2 - c ^ 2) / 2 - (d ^ 3 - c ^ 3) / 6 - (d - c) / (24 * b ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand_square_integral {b : ℝ} (hb : 0 < b) : ∫ (v : ↑unitInterval), Support.clampedSquare b (sourceBandIntercept b v) = if b ≤ 1 then 1 / 3 + b ^ 2 / 12 - b ^ 3 / 30 else 1 / 2 - 1 / (6 * b) + 1 / (20 * b ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand_weight_integral {b : ℝ} (hb : 0 < b) : ∫ (v : ↑unitInterval), Support.clampedWeight b (sourceBandIntercept b v) = if b ≤ 1 then 1 / 4 + b / 12 - b ^ 2 / 40 else 1 / 3 - 1 / (24 * b ^ 2) + 1 / (60 * b ^ 3)