Bernstein inequalities for band-limited functions

DefinitionHomogeneous Sobolev seminorm (band-limited derivative bound)#✓fully proved

For \(s \in \mathbb{R}\) and a Schwartz function \(f : \mathbb{R} \to \mathbb{C}\) with Fourier transform \(\hat f(\xi) = \int_{\mathbb{R}} f(x) e^{-2\pi i x\xi}\,dx\), the homogeneous Sobolev seminorm of order \(s\) 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 its integrand is not integrable.

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

Used by 1

Used byBernstein-type bound for the derivative of a band-limited Schwartz function

TheoremBernstein-type bound for the derivative of a band-limited Schwartz function#●ready to prove

Let \(s \in (\tfrac12, 1]\). For a Schwartz function \(f : \mathbb{R} \to \mathbb{C}\) write \(\hat f(\xi) = \int_{\mathbb{R}} f(x) e^{-2\pi i x\xi}\,dx\) for its Fourier transform and \(\|f\|_{\dot H^s} = \left(\int_{\mathbb{R}} |\xi|^{2s} |\hat f(\xi)|^2\,d\xi\right)^{1/2}\) for its homogeneous Sobolev seminorm. There is a constant \(C_1 > 0\) such that for every real \(A \ge 0\) and every Schwartz function \(f : \mathbb{R} \to \mathbb{C}\) with \(\hat f(\xi) = 0\) whenever \(|\xi| > A\),

\[\sup_{x \in \mathbb{R}} |f'(x)| \le C_1 A^{3/2 - s}\, \|f\|_{\dot H^s}.\]

public theorem_wanted norm_deriv_le_rpow_mul_dotHSeminorm_of_fourier_support_Icc
    (s : ℝ) (hs : s ∈ Set.Ioc (1 / 2 : ℝ) 1) :
    ∃ C1 > 0, ∀ (A : NNReal),
      ∀ f : SchwartzMap ℝ ℂ,
        Function.support (fun ξ : ℝ => (𝓕 f) ξ) ⊆ Set.Icc (-(A : ℝ)) (A : ℝ) →
          sSup (Set.range (fun x : ℝ => ‖deriv (fun y : ℝ => f y) x‖)) ≤
            C1 * Real.rpow (A : ℝ) (3 / 2 - s) *
              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_00.

Uses 1

Statement usesHomogeneous Sobolev seminorm (band-limited derivative bound)

TheoremBernstein inequality for Schwartz functions with Fourier support of finite measure#●ready to prove

Fix \(n \in \mathbb{N}\). For a Schwartz function \(f : \mathbb{R}^n \to \mathbb{C}\) write \(\hat f(\xi) = \int_{\mathbb{R}^n} f(x) e^{-2\pi i \langle x, \xi \rangle}\,dx\) for its Fourier transform, and write \(|E|\) for the Lebesgue measure of a set \(E \subseteq \mathbb{R}^n\). There is a constant \(C > 0\) such that for every Borel set \(E \subseteq \mathbb{R}^n\) with \(|E| < \infty\), all \(p, q \in [1, \infty]\) with \(p \le q\) and \(p \le 2\), and every Schwartz function \(f : \mathbb{R}^n \to \mathbb{C}\) whose Fourier transform has closed support \(\overline{\{\xi : \hat f(\xi) \ne 0\}}\) contained in \(E\),

\[\|f\|_{L^q(\mathbb{R}^n)} \le C\, |E|^{1/p - 1/q}\, \|f\|_{L^p(\mathbb{R}^n)},\]

where \(1/q = 0\) for \(q = \infty\).

MathlibExt.Analysis.Fourier.BernsteinFourierSupportLpLqWanted.exists_const_norm_toLp_le_volume_rpow_mul_norm_toLp_of_tsupport_fourier_subset · 17 lines

public theorem_wanted exists_const_norm_toLp_le_volume_rpow_mul_norm_toLp_of_tsupport_fourier_subset
    {n : ℕ} :
    ∃ C : ℝ, 0 < C ∧
      ∀ (E : Set (EuclideanSpace ℝ (Fin n))),
        MeasurableSet E →
        (MeasureTheory.volume E) < ⊤ →
        ∀ p q : ENNReal,
          1 ≤ p → p ≤ q → q ≤ ⊤ → p ≤ 2 →
            ∀ f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ,
              tsupport (fun ξ : EuclideanSpace ℝ (Fin n) => (𝓕 f) ξ) ⊆ E →
                ‖f.toLp q
                    (MeasureTheory.volume : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n)))‖ ≤
                  C *
                    Real.rpow (MeasureTheory.volume E).toReal
                      (1 / p.toReal -  (1 / q).toReal) *
                    ‖f.toLp p
                      (MeasureTheory.volume : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n)))‖

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Distributions, generalized functions, distribution spaces), problem ma_proofbench_l2_47.

TheoremBernstein inequality for band-limited Schwartz functions#●ready to prove

For a Schwartz function \(f : \mathbb{R} \to \mathbb{C}\) write \(\hat f(\xi) = \int_{\mathbb{R}} f(x) e^{-2\pi i x\xi}\,dx\) for its Fourier transform. There is a constant \(C_0 > 0\) such that for every \(p \in [1, \infty]\) and every Schwartz function \(f : \mathbb{R} \to \mathbb{C}\) with \(\hat f(\xi) = 0\) whenever \(|\xi| \ge 1\),

\[\|f'\|_{L^p(\mathbb{R})} \le C_0 \|f\|_{L^p(\mathbb{R})}.\]

public theorem_wanted exists_norm_deriv_toLp_le_of_support_fourier_subset_ball :
    ∃ C0 > 0, ∀ p : ENNReal,
      (1 : ENNReal) ≤ p  →
      ∀ f : SchwartzMap ℝ ℂ,
        Function.support (fun ξ : ℝ => (𝓕 f) ξ) ⊆ Metric.ball (0 : ℝ) 1 →
          ‖(SchwartzMap.derivCLM ℂ ℂ f).toLp p
              (MeasureTheory.volume : MeasureTheory.Measure ℝ)‖ ≤
            C0 * ‖f.toLp p (MeasureTheory.volume : MeasureTheory.Measure ℝ)‖

Sources

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

1 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.