← Mathematical handbook

CDF formulas for a standardized uniform band

theorem Verification.IncreasingBand.density_row_prefix (B : IncreasingBand) (u t : ↑unitInterval) : ∫ (v : ↑unitInterval) in Set.Iic t, B.density (u, v) = unitClamp ((↑t - B.lower u) / B.width)

theorem Verification.IncreasingBand.measure_prefix (B : IncreasingBand) (u t : ↑unitInterval) : B.measure.real (Set.Iic u ×ˢ Set.Iic t) = ∫ (s : ↑unitInterval) in Set.Iic u, unitClamp ((↑t - B.lower s) / B.width)

theorem Verification.IncreasingBand.marginal_prefix (B : IncreasingBand) (t : ↑unitInterval) : B.marginal.real (Set.Iic t) = ∫ (s : ↑unitInterval), unitClamp ((↑t - B.lower s) / B.width)

theorem Verification.IncreasingBand.copula_cdf (B : IncreasingBand) (u v : ↑unitInterval) : B.copula.cdf ![u, v] = ∫ (s : ↑unitInterval) in Set.Iic u, unitClamp ((↑(ProbabilityTheory.unitQuantile B.marginal v) - B.lower s) / B.width)

Quantile inversion identifies the standardized CDF, including null flat fibers.