Weighted bounds for the stable density

Differentiation under Fourier inversion and integration by parts give boundedness of the density and its derivative after multiplication by the spatial variable.

Reference: V. M. Zolotarev, One-dimensional Stable Distributions, AMS, 1986, Section 2.4.

theorem BGW.StableTrees.exists_abs_mul_stableDensity_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (C : ℝ), ∀ (x : ℝ), |x * Scalar.stableDensity θ x| ≤ C

sup_x |x p_1(x)| < ∞.

theorem BGW.StableTrees.differentiable_stableDensity {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : Differentiable ℝ (Scalar.stableDensity θ)

p_1 is differentiable.

theorem BGW.StableTrees.exists_abs_mul_deriv_stableDensity_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (C : ℝ), ∀ (x : ℝ), |x * deriv (Scalar.stableDensity θ) x| ≤ C

sup_x |x p_1'(x)| < ∞.