Fourier transform and uncertainty principles

The Fourier transform on R^n and Schwartz functions: convolution, Bochner, Hausdorff–Young, Heisenberg and fractal uncertainty, band-limited functions and Bernstein inequalities, sampling and Fourier interpolation, Kakeya sets, Beurling–Ahlfors and other singular integrals.

TheoremConvolution of two square-integrable functions is continuous and vanishes at infinity#●ready to prove

Let \(n\) be a natural number and let \(f, g : \mathbb{R}^n \to \mathbb{C}\) be square-integrable. Then the convolution \((f \ast g)(x) = \int_{\mathbb{R}^n} f(x - y) \, g(y) \, dy\) is a continuous function of \(x \in \mathbb{R}^n\), and \((f \ast g)(x) \to 0\) as \(|x| \to \infty\).

public theorem_wanted continuous_and_tendsto_cocompact_convolution_of_memLp_two
    (n : ℕ) (f g : (Fin n → ℝ) → ℂ)
    (hf : MemLp f 2 volume) (hg : MemLp g 2 volume) :
    Continuous (fun x : Fin n → ℝ => ∫ y, f (x - y) * g y) ∧
    Filter.Tendsto (fun x : Fin n → ℝ => ∫ y, f (x - y) * g y)
      (Filter.cocompact (Fin n → ℝ)) (nhds 0)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l2_17.

TheoremConvolution theorem#✓fully proved

Let \(e\) be a continuous additive character from \(\mathbb{R}\) to the unit circle, and let \(\mu\) be a σ-finite measure on \(\mathbb{R}\) that is preserved by every translation \(x \mapsto a + x\). For \(\varphi : \mathbb{R} \to \mathbb{C}\) write \(\hat\varphi(w) = \int e(-xw)\,\varphi(x)\,d\mu(x)\) for its Fourier transform with respect to \(e\) and \(\mu\), and for \(f, g : \mathbb{R} \to \mathbb{C}\) write \((f * g)(x) = \int f(t)\,g(x - t)\,d\mu(t)\) for their convolution. If \(f\) and \(g\) are \(\mu\)-integrable, then \(\widehat{f * g}(w) = \hat f(w)\,\hat g(w)\) for every \(w \in \mathbb{R}\).

Proof: Integrability of the convolution integrand, Fubini's theorem, translation invariance of \(\mu\) and multiplicativity of \(e\), following Stein--Shakarchi, Ch. 5, Prop. 1.11.

theorem convolution_theorem {e : AddChar ℝ Circle}
    {μ : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite μ] (he : Continuous e)
    (hinv : ∀ a : ℝ, MeasureTheory.MeasurePreserving (fun x => a + x) μ μ)
    {f g : ℝ → ℂ}
    (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ)
    (w : ℝ) :
    Fourier.fourierIntegral e μ
      (f ⋆[ContinuousLinearMap.lsmul ℂ ℂ, μ] g) w =
      Fourier.fourierIntegral e μ f w * Fourier.fourierIntegral e μ g w
Sources
  • https://en.wikipedia.org/wiki/Convolution_theorem.

TheoremHausdorff–Young inequality for Schwartz functions#●ready to prove

Let \(n\) be a natural number and let \(\mathcal{F}\) be the Fourier transform on \(\mathbb{R}^n\), \(\mathcal{F}f(\xi) = \int_{\mathbb{R}^n} f(x) e^{-2\pi i \langle x, \xi \rangle}\, dx\). There is a constant \(C > 0\) such that for all \(p, p' \in [0, \infty]\) with \(1 \le p \le 2\) and \(\frac{1}{p} + \frac{1}{p'} = 1\) (so \(p' = \infty\) when \(p = 1\)) and every complex-valued Schwartz function \(f\) on \(\mathbb{R}^n\), \(\|\mathcal{F}f\|_{L^{p'}} \le C \|f\|_{L^p}\), where the \(L^p\) norms are taken with respect to Lebesgue measure on \(\mathbb{R}^n\).

public theorem_wanted exists_norm_fourier_toLp_le_norm_toLp_of_holderConjugate
    {n : ℕ} :
    ∃ C : ℝ, 0 < C ∧
      ∀ p p' : ENNReal,
        1 ≤ p → p ≤ 2 → ENNReal.HolderConjugate p p' →
          ∀ f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ,
            ‖(𝓕 f).toLp p'
                (MeasureTheory.volume : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n)))‖ ≤
              C * ‖f.toLp p
                (MeasureTheory.volume : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n)))‖
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; General theory of linear operators), problem ma_proofbench_l2_84.
1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.