← Copula mathematical handbook

Exact marginal means of scaled clamped affine sections

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.unitClamp_positive_parts (x : ℝ) : unitClamp x = max 0 x - max 0 (x - 1)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.unitClamp_complement (x : ℝ) : unitClamp (1 - x) = 1 - unitClamp x

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

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

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

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

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.clampedMean_complement (b a : ℝ) : clampedMean b (b + 1 - a) = 1 - clampedMean b a