Sup-norm bounds for high-frequency functions

DefinitionHomogeneous Sobolev seminorm for the high-frequency sup-norm bound#✓fully proved

For a real number \(s\) and a Schwartz function \(f : \mathbb{R} \to \mathbb{C}\) with Fourier transform \(\hat f(\xi) = \int_{\mathbb{R}} e^{-2\pi i x \xi} f(x) \, dx\), the homogeneous Sobolev seminorm of \(f\) is

\[ \|f\|_{\dot H^s} = \left( \int_{\mathbb{R}} |\xi|^{2s} \, |\hat f(\xi)|^2 \, d\xi \right)^{1/2}, \]

where the integral is taken to be \(0\) when the integrand is not integrable.

noncomputable def dotHSeminorm (s : ℝ) (f : SchwartzMap ℝ ℂ) : ℝ :=
  Real.sqrt (∫ ξ : ℝ, Real.rpow ‖ξ‖ (2 * s) * ‖(𝓕 f) ξ‖ ^ 2)

Used by 1

Used bySup bound for Schwartz functions with high-frequency Fourier support

TheoremSup bound for Schwartz functions with high-frequency Fourier support#●ready to prove

Let \(s \in (\tfrac12, 1]\), and for a Schwartz function \(f : \mathbb{R} \to \mathbb{C}\) with Fourier transform \(\hat f\) let \(\|f\|_{\dot H^s} = \left( \int_{\mathbb{R}} |\xi|^{2s} |\hat f(\xi)|^2 \, d\xi \right)^{1/2}\) be its homogeneous Sobolev seminorm. There is a constant \(C_2 > 0\) such that for every real \(A > 0\) and every Schwartz function \(f : \mathbb{R} \to \mathbb{C}\) whose Fourier transform has closed support contained in \(\mathbb{R} \setminus [-A, A]\),

\[ \sup_{x \in \mathbb{R}} |f(x)| \le C_2 \, A^{-s + \frac12} \, \|f\|_{\dot H^s}. \]

public theorem_wanted sSup_norm_le_rpow_mul_dotHSeminorm_of_tsupport_fourier_compl_Icc
    (s : ℝ) (hs : s ∈ Set.Ioc (1 / 2 : ℝ) 1) :
    ∃ C2 > 0, ∀ (A : NNReal),
      0 < (A : ℝ) →
      ∀ f : SchwartzMap ℝ ℂ,
        tsupport (fun ξ : ℝ => (𝓕 f) ξ) ⊆ (Set.Icc (-(A : ℝ)) (A : ℝ))ᶜ →
          sSup (Set.range (fun x : ℝ => ‖f x‖)) ≤
            C2 * Real.rpow (A : ℝ) (-s + 1 / 2) * dotHSeminorm s f

Sources

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

Uses 1

Statement usesHomogeneous Sobolev seminorm for the high-frequency sup-norm bound

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.