Gagliardo–Nirenberg inequality

TheoremSixth-power integral bounded by the Dirichlet energy under \(L^2\) normalization#●ready to prove

There is a constant \(C_2 > 0\) such that every infinitely differentiable, compactly supported function \(u : \mathbb{R} \to \mathbb{R}\) with \(\int_{\mathbb{R}} u(t)^2 \, dt = 1\) satisfies

\[\int_{\mathbb{R}} u(t)^6 \, dt \le C_2 \int_{\mathbb{R}} u'(t)^2 \, dt.\]

public theorem_wanted exists_integral_pow_six_le_integral_deriv_sq_of_integral_sq_eq_one :
    ∃ C2 : ℝ, 0 < C2 ∧
      ∀ u : ℝ → ℝ,
        ContDiff ℝ (⊤ : ℕ∞) u →
        HasCompactSupport u →
        (∫ t, (u t) ^ 2) = 1 →
          ∫ t, (u t) ^ 6 ≤ C2 * ∫ t, (deriv u t) ^ 2

Sources

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

TheoremA weighted \(L^6\) bound with a slowly varying weight#●ready to prove

There is a constant \(C > 0\) with the following property. Let \(\theta : \mathbb{R} \to \mathbb{R}\) be continuously differentiable, with \(\theta(x) > 0\) for every \(x\) and \(\|\theta'/\theta\|_{L^\infty(\mathbb{R})} \le 1\), and let \(u : \mathbb{R} \to \mathbb{R}\) be smooth with compact support. Then

\[\int_{\mathbb{R}} u(x)^6\,\theta(x)\,dx \le C\,\|u\|_{L^2(\mathbb{R})}^4 \int_{\mathbb{R}} \left(|u'(x)|^2 + |u(x)|^2\right)\theta(x)\,dx.\]

public theorem_wanted exists_integral_pow_six_mul_weight_le :
    ∃ C : ℝ, 0 < C ∧
      ∀ (θ : ℝ → ℝ), (∀ x : ℝ, 0 < θ x) → ContDiff ℝ 1 θ →
        eLpNorm (fun x : ℝ => deriv θ x / θ x) ⊤ volume ≤ 1 →
        ∀ u : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) u → HasCompactSupport u →
          ∫ x : ℝ, (u x) ^ (6 : ℕ) * θ x ≤
            C * (ENNReal.toReal (eLpNorm u 2 volume)) ^ (4 : ℕ) *
              ∫ x : ℝ, (|deriv u x| ^ (2 : ℕ) + |u x| ^ (2 : ℕ)) * θ x

Sources

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

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.