← Mathematical handbook

Total positivity after standardizing an increasing fixed-width band

theorem Verification.IncreasingBand.density_tp2 (B : IncreasingBand) (hB : Monotone B.lower) : ProbabilityTheory.IsTP2 fun (u v : ↑unitInterval) => B.density (u, v)

theorem Verification.IncreasingBand.standardizedDensity_tp2 (B : IncreasingBand) (hB : Monotone B.lower) : ProbabilityTheory.IsTP2 fun (u v : ↑unitInterval) => B.standardizedDensity (u, v)

The density after the probability integral transform remains TP2.

theorem Verification.IncreasingBand.copula_hasMTP2Density (B : IncreasingBand) (hB : Monotone B.lower) : B.copula.HasMTP2Density

This is an MTP2 density of the actual standardized copula measure.