← Mathematical handbook

theorem Verification.tendsto_succ_pow_exp {f : ℕ → ℝ} {L : ℝ} (hf : Filter.Tendsto (fun (n : ℕ) => (↑n + 1) * (f n - 1)) Filter.atTop (nhds L)) : Filter.Tendsto (fun (n : ℕ) => f n ^ (n + 1)) Filter.atTop (nhds (Real.exp L))

theorem Verification.galambos_maxima_limit_interior (δ : ℝ) (hδ : 0 < δ) (u v : ↑unitInterval) (hu : ↑u ∈ Set.Ioo 0 1) (hv : ↑v ∈ Set.Ioo 0 1) : Filter.Tendsto (fun (n : ℕ) => (normalizedMaxima (ProbabilityTheory.Copula.clayton 2 δ hδ).survivalCopula n).cdf ![u, v]) Filter.atTop (nhds (↑u * ↑v * Real.exp (galambosTailKernel δ (-Real.log ↑u) (-Real.log ↑v))))

noncomputable def Verification.galambosCDF (δ : ℝ) (u : Fin 2 → ↑unitInterval) : ℝ

Equations

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

theorem Verification.galambos_maxima_limit (δ : ℝ) (hδ : 0 < δ) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (n : ℕ) => (normalizedMaxima (ProbabilityTheory.Copula.clayton 2 δ hδ).survivalCopula n).cdf u) Filter.atTop (nhds (galambosCDF δ u))

noncomputable def Verification.galambos (δ : ℝ) (hδ : 0 < δ) : ProbabilityTheory.Copula 2

Equations

• Verification.galambos δ hδ = ⋯.choose

theorem Verification.galambos_cdf (δ : ℝ) (hδ : 0 < δ) : (galambos δ hδ).cdf = galambosCDF δ