← Mathematical handbook

noncomputable def Verification.galambosTailKernel (δ x y : ℝ) : ℝ

Equations

• Verification.galambosTailKernel δ x y = (x ^ (-δ) + y ^ (-δ)) ^ (-1 / δ)

theorem Verification.clayton_scaled_cdf (δ : ℝ) (hδ : 0 < δ) (c : ℝ) (hc : 0 < c) (u v : ↑unitInterval) (hu : 0 < ↑u) (hv : 0 < ↑v) : c * (ProbabilityTheory.Copula.clayton 2 δ hδ).cdf ![u, v] = ((c * ↑u) ^ (-δ) + (c * ↑v) ^ (-δ) - c ^ (-δ)) ^ (-1 / δ)

theorem Verification.clayton_scaled_cdf_limit {ι : Type u_1} {l : Filter ι} (δ : ℝ) (hδ : 0 < δ) (c : ι → ℝ) (hc : ∀ (i : ι), 0 < c i) (hctop : Filter.Tendsto c l Filter.atTop) (u v : ι → ↑unitInterval) (hu : ∀ (i : ι), 0 < ↑(u i)) (hv : ∀ (i : ι), 0 < ↑(v i)) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hux : Filter.Tendsto (fun (i : ι) => c i * ↑(u i)) l (nhds x)) (hvy : Filter.Tendsto (fun (i : ι) => c i * ↑(v i)) l (nhds y)) : Filter.Tendsto (fun (i : ι) => c i * (ProbabilityTheory.Copula.clayton 2 δ hδ).cdf ![u i, v i]) l (nhds (galambosTailKernel δ x y))