← Copula mathematical handbook

Exact area of a median tent

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.Support.integral_medianTent {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : ∫ (v : ↑unitInterval), medianTent r ↑v = r ^ 2 / 4

Includes the degenerate tent r=0 and the full-width tent r=1.