← Mathematical handbook

noncomputable def Verification.gbPsi (θ t : ℝ) : ℝ

Equations

• Verification.gbPsi θ t = Real.exp ((1 - Real.exp t) / θ)

theorem Verification.gbPsi_derivative (θ t : ℝ) : HasDerivAt (gbPsi θ) (-Real.exp t / θ * gbPsi θ t) t

theorem Verification.gbPsi_second_derivative (θ t : ℝ) (hθ : θ ≠ 0) : HasDerivAt (fun (x : ℝ) => -Real.exp x / θ * gbPsi θ x) (Real.exp t * (Real.exp t - θ) / θ ^ 2 * gbPsi θ t) t

theorem Verification.gbPsi_convex (θ : ℝ) (hθ : 0 < θ) (hθ1 : θ ≤ 1) : ConvexOn ℝ (Set.Ici 0) (gbPsi θ)

noncomputable def Verification.gumbelBarnettGenerator (θ : ℝ) (hθ : 0 < θ) (hθ1 : θ ≤ 1) : ProbabilityTheory.Copula.BivariateGenerator

An admissible bivariate Gumbel–Barnett generator.

Equations

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

noncomputable def Verification.gumbelBarnett (θ : ↑unitInterval) : ProbabilityTheory.Copula 2

The family on its closed parameter interval, with independence at zero.

Equations

• Verification.gumbelBarnett θ = if h : ↑θ = 0 then ProbabilityTheory.Copula.independence 2 else (Verification.gumbelBarnettGenerator ↑θ ⋯ ⋯).copula

theorem Verification.gumbelBarnett_zero : gumbelBarnett 0 = ProbabilityTheory.Copula.independence 2

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

theorem Verification.gumbelBarnett_transpose (θ : ↑unitInterval) : (gumbelBarnett θ).transpose = gumbelBarnett θ