Convolution asymptotics of subexponential functions

DefinitionThe function \(e^{-\sqrt{\|x\|}}\) on the plane#✓fully proved

Let \(f : \mathbb{R}^2 \to \mathbb{R}\) be \(f(x) = e^{-\sqrt{\|x\|}}\), where \(\|x\|\) is the Euclidean norm of \(x\).

noncomputable def f : EuclideanSpace ℝ (Fin 2) → ℝ := fun x =>
  Real.exp (-(Real.sqrt ‖x‖))

Used by 1

Used byAsymptotics of the self-convolution of \(e^{-\sqrt{\|x\|}}\)

TheoremAsymptotics of the self-convolution of \(e^{-\sqrt{\|x\|}}\)#●ready to prove

Let \(f : \mathbb{R}^2 \to \mathbb{R}\) be \(f(x) = e^{-\sqrt{\|x\|}}\), where \(\|x\|\) is the Euclidean norm, and let \(f * f\) be the convolution of \(f\) with itself with respect to Lebesgue measure. Then

\[\lim_{\|a\| \to \infty} \frac{(f * f)(a)}{f(a)} = 2 \int_{\mathbb{R}^2} f(x)\,dx.\]

public theorem_wanted tendsto_convolution_self_div_atTop_norm :
    Filter.Tendsto
      (fun a : EuclideanSpace ℝ (Fin 2) => ((f ⋆ f) a) / f a)
      (Filter.comap (fun a : EuclideanSpace ℝ (Fin 2) => ‖a‖) Filter.atTop)
      (nhds (2 * ∫ x : EuclideanSpace ℝ (Fin 2), f x))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Measures, integration, derivative, holomorphy), problem ma_proofbench_l2_90.

Uses 1

Statement usesThe function \(e^{-\sqrt{\|x\|}}\) on the plane

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.