← Mathematical handbook

An MTP2 density for the actual quadratic-band copula

noncomputable def Verification.quadraticRawBand (b : ℝ) (hb : 0 ≤ b) : IncreasingBand

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.quadraticRawBand_lower_monotone (b : ℝ) (hb : 0 ≤ b) : Monotone (quadraticRawBand b hb).lower

theorem Verification.quadraticRawBand_ratio (b : ℝ) (hb : 0 ≤ b) (t u : ↑unitInterval) : (↑t - (quadraticRawBand b hb).lower u) / (quadraticRawBand b hb).width = (b + 1) * ↑t - b + b * (1 - ↑u) ^ 2

theorem Verification.quadraticRawBand_intercept_mem (b : ℝ) (hb : 0 ≤ b) (t : ↑unitInterval) : (b + 1) * ↑t - b ∈ Set.Icc (-b) 1

theorem Verification.quadraticRawBand_marginal (b : ℝ) (hb : 0 ≤ b) (t : ↑unitInterval) : unitCDF (quadraticRawBand b hb).marginal t = quadraticMeanUnit b ((b + 1) * ↑t - b)

theorem Verification.quadraticRawBand_copula (b : ℝ) (hb : 0 ≤ b) : (quadraticRawBand b hb).copula = quadraticBand b hb

The positive band construction equals the previously constructed extremal copula.

theorem Verification.quadraticBand_hasMTP2Density (b : ℝ) (hb : 0 ≤ b) : (quadraticBand b hb).HasMTP2Density

Every finite nonnegative parameter has a genuine Lebesgue MTP2 density.