← Mathematical handbook

theorem Verification.galambos_kernel_bound (δ : ℝ) (hδ : 0 < δ) (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : galambosTailKernel δ x y ≤ max x y * 2 ^ (-1 / δ)

theorem Verification.galambos_kernel_limit_zero {ι : Type u_1} {l : Filter ι} (δ : ι → ℝ) (hδ : ∀ (i : ι), 0 < δ i) (hd : Filter.Tendsto δ l (nhds 0)) (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : Filter.Tendsto (fun (i : ι) => galambosTailKernel (δ i) x y) l (nhds 0)