← Mathematical handbook

theorem Verification.gumbelBarnett_cdf_power (θ u v : ↑unitInterval) : (gumbelBarnett θ).cdf ![u, v] = ↑v * ↑u ^ (1 - ↑θ * Real.log ↑v)

theorem Verification.gumbelBarnett_isSD (θ : ↑unitInterval) : (gumbelBarnett θ).IsSD

theorem Verification.gumbelBarnett_isCD (θ : ↑unitInterval) : (gumbelBarnett θ).IsCD

theorem Verification.gumbelBarnett_isPQD_iff (θ : ↑unitInterval) : (gumbelBarnett θ).IsPQD ↔ θ = 0

theorem Verification.gumbelBarnett_isCI_iff (θ : ↑unitInterval) : (gumbelBarnett θ).IsCI ↔ θ = 0

theorem Verification.gumbelBarnett_density_tp2_iff (θ : ↑unitInterval) : (gumbelBarnett θ).HasMTP2Density ↔ θ = 0

theorem Verification.gumbelBarnett_lowerOrthant_iff (θ η : ↑unitInterval) : (gumbelBarnett θ).LowerOrthantLE (gumbelBarnett η) ↔ η ≤ θ

theorem Verification.gumbelBarnett_schur_iff (θ η : ↑unitInterval) : (gumbelBarnett θ).SchurBothLE (gumbelBarnett η) ↔ θ ≤ η

theorem Verification.gumbelBarnett_tails (θ : ↑unitInterval) : (gumbelBarnett θ).HasLowerTailDependence 0 ∧ (gumbelBarnett θ).HasUpperTailDependence 0

theorem Verification.gumbelBarnett_cdf_parameter_continuous (u v : ↑unitInterval) : Continuous fun (θ : ↑unitInterval) => (gumbelBarnett θ).cdf ![u, v]