← Mathematical handbook

noncomputable def Verification.gbExponent (θ v : ↑unitInterval) : ℝ

Equations

• Verification.gbExponent θ v = 1 - ↑θ * Real.log ↑v

theorem Verification.gbExponent_ge_one (θ v : ↑unitInterval) : 1 ≤ gbExponent θ v

noncomputable def Verification.gbConditional (θ u v : ↑unitInterval) : ℝ

Equations

• Verification.gbConditional θ u v = ↑v * Verification.gbExponent θ v * ↑u ^ (Verification.gbExponent θ v - 1)

theorem Verification.gumbelBarnett_conditionalCDF (θ v : ↑unitInterval) : (fun (u : ↑unitInterval) => (gumbelBarnett θ).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => gbConditional θ u v

theorem Verification.integral_gbConditional_sq (θ v : ↑unitInterval) : ∫ (u : ↑unitInterval), gbConditional θ u v ^ 2 = ↑v ^ 2 * gbExponent θ v ^ 2 / (2 * gbExponent θ v - 1)

theorem Verification.gumbelBarnett_xi_integral (θ : ↑unitInterval) : (gumbelBarnett θ).chatterjeeXi = (6 * ∫ (v : ↑unitInterval), ↑v ^ 2 * gbExponent θ v ^ 2 / (2 * gbExponent θ v - 1)) - 2

theorem Verification.gumbelBarnett_chatterjeeXi (θ : ↑unitInterval) (hθ : 0 < ↑θ) : (gumbelBarnett θ).chatterjeeXi = 3 * Real.exp (3 / (2 * ↑θ)) / (4 * ↑θ) * exponentialIntegralE1 (3 / (2 * ↑θ)) + ↑θ / 3 - 1 / 2