Function spaces and Sobolev inequalities

L^p and Sobolev spaces of functions: embeddings (Morrey, Rellich, radial, trace), Ehrling, Agmon, Ladyzhenskaya, Gagliardo–Nirenberg and weighted Hardy–Sobolev inequalities, sup-norm bounds by H¹ energy, L^p limits and weak convergence in L^p.

• Gagliardo–Nirenberg inequality
• Radial Sobolev embedding
• Rellich–Kondrachov theorem
• Sobolev embedding theorem
• Sup-norm bounds by derivatives on an interval
• Sup-norm bounds for high-frequency functions
• Weighted Hardy–Sobolev inequalities on an annulus

TheoremAgmon's inequality on the line#●ready to prove

There is a constant \(C > 0\) such that every real-valued Schwartz function \(f \colon \mathbb{R} \to \mathbb{R}\) satisfies

\[\|f\|_{L^\infty} \le C \, \|f\|_{L^2}^{1/2} \, \|f'\|_{L^2}^{1/2},\]

where \(f'\) is the derivative of \(f\) and the \(L^\infty\) and \(L^2\) norms are taken with respect to Lebesgue measure on \(\mathbb{R}\).

public theorem_wanted exists_norm_toLp_top_le_mul_sqrt_norm_toLp_two_mul_sqrt_deriv :
    ∃ C > 0, ∀ f : SchwartzMap ℝ ℝ,
      ‖f.toLp (⊤ : ENNReal) (MeasureTheory.volume : MeasureTheory.Measure ℝ)‖ ≤
        C * Real.sqrt ‖f.toLp (2 : ENNReal) (MeasureTheory.volume : MeasureTheory.Measure ℝ)‖ *
          Real.sqrt
            ‖(SchwartzMap.derivCLM ℝ ℝ f).toLp
                (2 : ENNReal) (MeasureTheory.volume : MeasureTheory.Measure ℝ)‖

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Real functions; Inequalities in real analysis), problem ma_proofbench_l2_94.

TheoremClosed subspaces of \(L^2((0,1))\) inside \(C((0,1))\) are finite-dimensional#●ready to prove

Let \(H\) be a closed linear subspace of the real space \(L^2([0,1])\) with respect to Lebesgue measure, and suppose that every element of \(H\) is the class of a continuous function \([0,1] \to \mathbb{R}\). Then \(H\) is finite-dimensional.

public theorem_wanted finiteDimensional_of_isClosed_of_le_range_toLp
    (H : Submodule ℝ (MeasureTheory.Lp ℝ (2 : ENNReal)
        (MeasureTheory.volume : MeasureTheory.Measure (Set.Icc (0 : ℝ) 1))))
    (hclosed : IsClosed (H : Set (MeasureTheory.Lp ℝ (2 : ENNReal)
          (MeasureTheory.volume : MeasureTheory.Measure (Set.Icc (0 : ℝ) 1)))))
    (hsubset : H ≤ (ContinuousMap.toLp (E := ℝ) (p := (2 : ENNReal))
        (MeasureTheory.volume : MeasureTheory.Measure (Set.Icc (0 : ℝ) 1)) ℝ).range) :
    FiniteDimensional ℝ ↥H

Sources

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

TheoremEhrling's inequality#●ready to prove

Let \(X\), \(Y\), \(Z\) be real Banach spaces, let \(i \colon X \to Y\) be an injective compact bounded linear operator, and let \(j \colon Y \to Z\) be an injective bounded linear operator. Then for every \(\varepsilon > 0\) there is \(C_\varepsilon > 0\) such that \(\|i(u)\|_Y \le \varepsilon \|u\|_X + C_\varepsilon \|j(i(u))\|_Z\) for all \(u \in X\).

public theorem_wanted ehrling_inequality
    {X Y Z : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y]
    [NormedAddCommGroup Z] [NormedSpace ℝ Z] [CompleteSpace Z]
    (iXY : X →L[ℝ] Y) (iYZ : Y →L[ℝ] Z)
    (hXY_compact : IsCompactOperator (iXY : X → Y))
    (hXY_inj : Function.Injective iXY)
    (hYZ_inj : Function.Injective iYZ) :
    ∀ ε > 0, ∃ Cε > 0, ∀ u : X,
      ‖iXY u‖ ≤ ε * ‖u‖ + Cε * ‖iYZ (iXY u)‖

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Normed linear spaces and Banach spaces; Banach lattices), problem ma_proofbench_l2_36.

TheoremNonlinear interpolation of Lipschitz maps on Lebesgue spaces (Scottish Book Problem 87)#●ready to prove

Let \(\mu\) be Lebesgue measure on \([0, 1]\), write \(\|f\|_p\) for the \(L^p(\mu)\) norm, let \(1 \le \beta < \alpha \le \infty\), and let \(U\) map functions \(\mathbb{R} \to \mathbb{R}\) to functions \(\mathbb{R} \to \mathbb{R}\). Suppose that \(U\) maps \(L^\beta(\mu)\) into \(L^\beta(\mu)\); that there is \(L \ge 0\) with \(\|Ux - Uy\|_\beta \le L \|x - y\|_\beta\) for all \(x, y \in L^\beta(\mu)\); and that there is \(M_\alpha \ge 0\) such that every \(x \in L^\alpha(\mu)\) has \(Ux \in L^\alpha(\mu)\) and \(\|Ux\|_\alpha \le M_\alpha \|x\|_\alpha\). Then for every \(\gamma\) with \(\beta < \gamma < \alpha\) there is \(M_\gamma \ge 0\) such that every \(x \in L^\gamma(\mu)\) has \(Ux \in L^\gamma(\mu)\) and \(\|Ux\|_\gamma \le M_\gamma \|x\|_\gamma\).

MathlibExt.Analysis.FunctionalAnalysis.ScottishBook87Wanted.nonlinearInterpolationLp · 28 lines

theorem_wanted nonlinearInterpolationLp :
    ∀ (β α : ℝ≥0∞) (hβ : 1 ≤ β) (hα : β < α)
      (U : (ℝ → ℝ) → (ℝ → ℝ)),
      (∃ L : ℝ, 0 ≤ L ∧ ∀ x y : ℝ → ℝ,
        MeasureTheory.MemLp x β (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)) →
        MeasureTheory.MemLp y β (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)) →
        (MeasureTheory.eLpNorm (U x - U y) β
          (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1))).toReal ≤
          L * (MeasureTheory.eLpNorm (x - y) β
            (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1))).toReal) →
      (∀ x : ℝ → ℝ,
        MeasureTheory.MemLp x β (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)) →
        MeasureTheory.MemLp (U x) β (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1))) →
      (∃ Mα : ℝ, 0 ≤ Mα ∧ ∀ x : ℝ → ℝ,
        MeasureTheory.MemLp x α (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)) →
        MeasureTheory.MemLp (U x) α (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)) ∧
        (MeasureTheory.eLpNorm (U x) α
          (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1))).toReal ≤
          Mα * (MeasureTheory.eLpNorm x α
            (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1))).toReal) →
      ∀ γ : ℝ≥0∞, β < γ → γ < α →
        ∃ Mγ : ℝ, 0 ≤ Mγ ∧ ∀ x : ℝ → ℝ,
          MeasureTheory.MemLp x γ (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)) →
          MeasureTheory.MemLp (U x) γ (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)) ∧
          (MeasureTheory.eLpNorm (U x) γ
            (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1))).toReal ≤
            Mγ * (MeasureTheory.eLpNorm x γ
              (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1))).toReal

Sources

• S. Banach, Problem 87 of the Scottish Book; affirmative solution by L. Maligranda, commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015). The linear case follows from the Riesz interpolation theorem, and Banach showed the case α = ∞; Maligranda's solution covers the nonlinear case as stated here, with α = ⊤ allowed.

TheoremSobolev trace bound on the plane \(z = 0\) in \(\mathbb{R}^3\)#●ready to prove

Let \((f_n)_{n \in \mathbb{N}}\) be a sequence of continuously differentiable functions \(\mathbb{R}^3 \to \mathbb{R}\), where \(\mathbb{R}^3\) has coordinates \((x, y, z)\) and the max norm. For \(p \in \mathbb{R}^3\) write \(\|Df_n(p)\|\) for the operator norm of the derivative of \(f_n\) at \(p\), which equals \(|\partial_x f_n(p)| + |\partial_y f_n(p)| + |\partial_z f_n(p)|\), the sum of the absolute values of the partial derivatives. Suppose that for every \(n\) the function \(p \mapsto |f_n(p)|^2 + \|Df_n(p)\|^2\) is Lebesgue integrable on \(\mathbb{R}^3\) with integral at most \(1\). Then there is a constant \(C \ge 0\) such that for every \(n\) the function \((x, y) \mapsto |f_n(x, y, 0)|^2\) is Lebesgue integrable on \(\mathbb{R}^2\) with integral at most \(C\).

Since \(\|Df_n(p)\|\) is at least the Euclidean length \(|\nabla f_n(p)|\) of the gradient, the hypothesis implies the bound \(\int_{\mathbb{R}^3} (|\nabla f_n|^2 + |f_n|^2) \le 1\) of the source problem; conversely, if \(f_n\) satisfies that bound, then \(f_n / \sqrt{3}\) satisfies the hypothesis.

public theorem_wanted exists_bound_integral_sq_trace_of_integral_sq_add_fderiv_sq_le_one
    (f : ℕ → ℝ × ℝ × ℝ → ℝ)
    (hC1 : ∀ n : ℕ, ContDiff ℝ 1 (f n))
    (henergy : ∀ n : ℕ,
      MeasureTheory.Integrable
      (fun x : ℝ × ℝ × ℝ => ‖f n x‖ ^ 2 + ‖fderiv ℝ (f n) x‖ ^ 2) MeasureTheory.volume ∧
      (∫ x : ℝ × ℝ × ℝ,
        (‖f n x‖ ^ 2 + ‖fderiv ℝ (f n) x‖ ^ 2) ∂MeasureTheory.volume) ≤ 1) :
    ∃ C : ℝ, 0 ≤ C ∧
      ∀ n : ℕ,
        MeasureTheory.Integrable
        (fun p : ℝ × ℝ => ‖f n (p.1, p.2, 0)‖ ^ 2) MeasureTheory.volume ∧
        (∫ p : ℝ × ℝ, ‖f n (p.1, p.2, 0)‖ ^ 2 ∂MeasureTheory.volume) ≤ C

Sources

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

TheoremThe constant in Young's \(L^1\)–\(L^p\) convolution inequality cannot be lowered#●ready to prove

Let \(1 \le p \le \infty\) and \(\varepsilon > 0\). Then there exist real-valued functions \(f \in L^1(\mathbb{R})\) and \(g \in L^p(\mathbb{R})\) such that

\[ \|f * g\|_p > (1 - \varepsilon) \|f\|_1 \|g\|_p, \]

where \((f * g)(x) = \int_{\mathbb{R}} f(t)\, g(x - t)\, dt\) and all norms are taken with respect to Lebesgue measure.

public theorem_wanted exists_eLpNorm_convolution_gt_one_sub_mul
    (p : ENNReal) (hp : 1 ≤ p) (ε : ℝ) (hε : 0 < ε) :
    ∃ (f g : ℝ → ℝ), MemLp f 1 ∧ MemLp g p ∧
      (eLpNorm (f ⋆ g) p).toReal > ((1 - ε) * (eLpNorm f 1).toReal * (eLpNorm g p).toReal)

Sources

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

TheoremWeighted Ladyzhenskaya inequality in the plane#●ready to prove

There is a constant \(C > 0\) such that for every \(C^1\) function \(\omega : \mathbb{R}^2 \to \mathbb{R}\) with \(\omega(x) > 0\) for all \(x\) and \(\|\nabla\omega/\omega\|_{L^\infty(\mathbb{R}^2)} \le 1\), and every smooth compactly supported function \(u : \mathbb{R}^2 \to \mathbb{R}\),

\[ \int_{\mathbb{R}^2} u^4 \omega \le C \|u\|_{L^2(\mathbb{R}^2)}^2 \int_{\mathbb{R}^2} \left(|\nabla u|^2 + |u|^2\right) \omega. \]

public theorem_wanted exists_const_integral_pow_four_mul_weight_le :
  ∃ C : ℝ, 0 < C ∧
    ∀ w : EuclideanSpace ℝ (Fin 2) → ℝ,
      (∀ x : EuclideanSpace ℝ (Fin 2), 0 < w x) →
      ContDiff ℝ 1 w →
      eLpNorm (fun x : EuclideanSpace ℝ (Fin 2) => ‖fderiv ℝ w x‖ / w x) ⊤ volume ≤ 1 →
      ∀ u : EuclideanSpace ℝ (Fin 2) → ℝ, ContDiff ℝ ∞ u → HasCompactSupport u →
        ∫ x : EuclideanSpace ℝ (Fin 2), (u x) ^ (4 : ℕ) * w x ≤
          C * (ENNReal.toReal (eLpNorm u 2 volume)) ^ (2 : ℕ) *
            ∫ x : EuclideanSpace ℝ (Fin 2), (‖fderiv ℝ u x‖ ^ (2 : ℕ) + |u x| ^ (2 : ℕ)) * w x

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Real functions; Inequalities in real analysis), problem ma_proofbench_l2_48.

7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.