Convolution

TheoremConvolution of an integrable and a bounded function is uniformly continuous#●ready to prove

Let \(d \in \mathbb{N}\), let \(f : \mathbb{R}^d \to \mathbb{R}\) be Lebesgue integrable, and let \(g : \mathbb{R}^d \to \mathbb{R}\) be Borel measurable and bounded. Then the convolution

\[ (f * g)(x) = \int_{\mathbb{R}^d} f(x - y)\, g(y)\, dy \]

is uniformly continuous on \(\mathbb{R}^d\).

public theorem_wanted uniformContinuous_convolution_integrable_bounded (d : ℕ)
    (f g : (Fin d → ℝ) → ℝ) (hf : MeasureTheory.Integrable f)
    (hg_meas : Measurable g)
    (hg_bdd : Bornology.IsBounded (Set.range g)) :
    UniformContinuous
      (fun x =>
        ∫ y, (f (x - y)) * (g y))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l1_15.

TheoremIntegrability of the convolution integrand#●ready to prove

Let \(d \in \mathbb{N}\) and let \(f, g : \mathbb{R}^d \to \mathbb{R}\) be Lebesgue integrable. Identify \(\mathbb{R}^{2d}\) with \(\mathbb{R}^d \times \mathbb{R}^d\) by writing a point as \((x, y)\), where \(x\) consists of its first \(d\) coordinates and \(y\) of its last \(d\) coordinates. Then the function \((x, y) \mapsto f(x - y)\, g(y)\) is Lebesgue integrable on \(\mathbb{R}^{2d}\).

public theorem_wanted integrable_comp_sub_mul_of_integrable_fin_append
    {d : ℕ} {f g : (Fin d → ℝ) → ℝ}
    (hf : Integrable f) (hg : Integrable g) :
    Integrable (fun p : Fin (d + d) → ℝ =>
        f (fun i : Fin d => p (Fin.castAdd d i) - p (Fin.natAdd d i)) *
        g (fun i : Fin d => p (Fin.natAdd d i)))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Measure and integration; Classical measure theory), problem ma_proofbench_l1_72.

TheoremExponential kernel approximate identity#●ready to prove

For every function \(f : \mathbb{R} \to \mathbb{R}\) in \(L^2(\mathbb{R})\),

\[ \lim_{n\to\infty} n\int_{\mathbb{R}}\int_{\mathbb{R}} f(x)f(y)e^{-2n|x-y|}\,dy\,dx = \int_{\mathbb{R}} f(x)^2\,dx, \]

where \(n\) runs through the natural numbers and the integrals are with respect to Lebesgue measure.

public theorem_wanted tendsto_mul_integral_integral_exp_neg_two_mul_abs_sub
  (f : ℝ → ℝ)
  (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  Filter.Tendsto
    (fun n : ℕ =>
      (n : ℝ) * (∫ x : ℝ, ∫ y : ℝ, f x * f y * Real.exp (-2 * (n : ℝ) * |x - y|)))
    Filter.atTop
    (nhds (∫ x : ℝ, f x ^ (2 : ℕ)))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_96.

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.