← Mathematical handbook

Singular mass and the exact density-TP2 classification of Cuadras–Augé

theorem Verification.powerSample_mono (a : ↑unitInterval) : Monotone (ProbabilityTheory.Copula.powerSample a)

theorem Verification.powerSample_unitPower (a : ↑unitInterval) (ha : 0 < a) (u : ↑unitInterval) : ProbabilityTheory.Copula.powerSample a (ProbabilityTheory.Copula.unitPower u ↑a ⋯) = u

theorem Verification.cuadrasAuge_diagonal_ne_zero (δ : ↑unitInterval) (hδ : 0 < δ) : (ProbabilityTheory.Copula.cuadrasAuge δ).toMeasure {x : Fin 2 → ↑unitInterval | x 0 = x 1} ≠ 0

A positive common-shock parameter puts positive mass on the diagonal.

theorem Verification.cuadrasAuge_absolutelyContinuous_iff (δ : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge δ).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ δ = 0

theorem Verification.cuadrasAuge_density_tp2_iff (δ : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge δ).HasMTP2Density ↔ δ = 0