← Mathematical handbook

theorem Verification.integral_unit_neg_exp_rpow {p : ℝ} (hp : 0 < p) (f : ℝ → ℝ) : ∫ (u : ↑unitInterval), f ↑u = ∫ (t : ℝ) in Set.Ioi 0, p * t ^ (p - 1) * Real.exp (-t ^ p) * f (Real.exp (-t ^ p))

theorem Verification.gumbelInv_generator {θ t : ℝ} (hθ : 0 < θ) (ht : 0 < t) : gumbelInv θ (Real.exp (-t ^ θ⁻¹)) = t

theorem Verification.gumbelWeight_generator {θ t : ℝ} (hθ : 0 < θ) (ht : 0 < t) : θ⁻¹ * t ^ (θ⁻¹ - 1) * Real.exp (-t ^ θ⁻¹) * gumbelWeight θ (Real.exp (-t ^ θ⁻¹)) = 1

theorem Verification.gumbel_product_generator {θ x y : ℝ} (hθ : 0 < θ) (hx : 0 < x) (hy : 0 < y) : θ⁻¹ * x ^ (θ⁻¹ - 1) * Real.exp (-x ^ θ⁻¹) * (θ⁻¹ * y ^ (θ⁻¹ - 1) * Real.exp (-y ^ θ⁻¹) * (gumbelPartial θ (Real.exp (-x ^ θ⁻¹)) (Real.exp (-y ^ θ⁻¹)) * gumbelPartial θ (Real.exp (-y ^ θ⁻¹)) (Real.exp (-x ^ θ⁻¹)))) = gumbelPsiDeriv θ⁻¹ (x + y) ^ 2

theorem Verification.gumbel_cdfSection_deriv {θ : ℝ} (hθ : 1 ≤ θ) (v : ↑unitInterval) (hv : ↑v ∈ Set.Ioo 0 1) (u : ℝ) (hu : u ∈ Set.Ioo 0 1) : HasDerivAt ((ProbabilityTheory.Copula.gumbel θ hθ).cdfSection v) (gumbelPartial θ u ↑v) u

theorem Verification.gumbel_conditionalCDF {θ : ℝ} (hθ : 1 ≤ θ) (v : ↑unitInterval) (hv : ↑v ∈ Set.Ioo 0 1) : (fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.gumbel θ hθ).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => gumbelPartial θ ↑u ↑v

theorem Verification.gumbel_transpose {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).transpose = ProbabilityTheory.Copula.gumbel θ hθ

theorem Verification.gumbel_conditionalCDF_ae {θ : ℝ} (hθ : 1 ≤ θ) : ∀ᵐ (v : ↑unitInterval) (u : ↑unitInterval), (ProbabilityTheory.Copula.gumbel θ hθ).conditionalCDF u v = gumbelPartial θ ↑u ↑v

theorem Verification.gumbel_kendallTau_integral {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).kendallTau = 1 - 4 * ∫ (u : ↑unitInterval) (v : ↑unitInterval), gumbelPartial θ ↑u ↑v * gumbelPartial θ ↑v ↑u

theorem Verification.gumbel_kendallTau_generator_integral {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).kendallTau = 1 - 4 * ∫ (x : ℝ) (y : ℝ) in Set.Ioi 0, gumbelPsiDeriv θ⁻¹ (x + y) ^ 2