← Mathematical handbook

Exact squared integral of a median tent

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBeta.medianTent (r v : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBeta.medianTent r v = max 0 (r / 2 - |v - 1 / 2|)

theorem ProbabilityTheory.Copula.RankRegion.XiBeta.continuous_medianTent (r : ℝ) : Continuous (medianTent r)

theorem ProbabilityTheory.Copula.RankRegion.XiBeta.medianTent_lipschitz (r v w : ℝ) : |medianTent r v - medianTent r w| ≤ |v - w|

theorem ProbabilityTheory.Copula.RankRegion.XiBeta.integral_medianTent_sq {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : ∫ (v : ↑unitInterval), medianTent r ↑v ^ 2 = r ^ 3 / 12

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