← Copula mathematical handbook

Polynomial moments of all clamped-affine section regimes

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.integral_positive_ramp_sq {b a : ℝ} (hb : 0 < b) (ha : 0 ≤ a) (hab : a ≤ b) : ∫ (u : ↑unitInterval), max 0 (a - b * ↑u) ^ 2 = a ^ 3 / (3 * b)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.integral_id_positive_ramp {b a : ℝ} (hb : 0 < b) (ha : 0 ≤ a) (hab : a ≤ b) : ∫ (u : ↑unitInterval), ↑u * max 0 (a - b * ↑u) = a ^ 3 / (6 * b ^ 2)

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedSquare (b a : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedSquare b a = ∫ (u : ↑unitInterval), ProbabilityTheory.Copula.RankRegion.Common.unitClamp (a - b * ↑u) ^ 2

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedWeight (b a : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedWeight b a = ∫ (u : ↑unitInterval), (1 - ↑u) * ProbabilityTheory.Copula.RankRegion.Common.unitClamp (a - b * ↑u)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedSquare_lower {b a : ℝ} (hb : 0 < b) (ha : 0 ≤ a) (hab : a ≤ b) (ha1 : a ≤ 1) : clampedSquare b a = a ^ 3 / (3 * b)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedWeight_lower {b a : ℝ} (hb : 0 < b) (ha : 0 ≤ a) (hab : a ≤ b) (ha1 : a ≤ 1) : clampedWeight b a = a ^ 2 / (2 * b) - a ^ 3 / (6 * b ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedSquare_affine {b a : ℝ} (hb : 0 ≤ b) (hba : b ≤ a) (ha1 : a ≤ 1) : clampedSquare b a = a ^ 2 - a * b + b ^ 2 / 3

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedWeight_affine {b a : ℝ} (hb : 0 ≤ b) (hba : b ≤ a) (ha1 : a ≤ 1) : clampedWeight b a = a / 2 - b / 6

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedSquare_saturated {b a : ℝ} (hb : 0 < b) (ha1 : 1 ≤ a) (hab : a ≤ b) : clampedSquare b a = (a - 2 / 3) / b

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedWeight_saturated {b a : ℝ} (hb : 0 < b) (ha1 : 1 ≤ a) (hab : a ≤ b) : clampedWeight b a = (a - 1 / 2) / b - (a ^ 2 - a + 1 / 3) / (2 * b ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedSquare_complement (b a : ℝ) : clampedSquare b (b + 1 - a) = 1 - 2 * clampedMean b a + clampedSquare b a

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedWeight_complement (b a : ℝ) : clampedWeight b (b + 1 - a) = 1 / 2 - clampedMean b a + clampedWeight b a