Sup-norm bounds by derivatives on an interval

TheoremSup norm on \((0,1)\) bounded by the derivative and the \(L^1\) norm#●ready to prove

For every \(\varepsilon > 0\) there is a constant \(C_\varepsilon > 0\) such that every function \(f : \mathbb{R} \to \mathbb{R}\) that is continuously differentiable on \([0,1]\) satisfies

\[\sup_{x \in [0,1]} |f(x)| \le \varepsilon \sup_{x \in [0,1]} |f'(x)| + C_\varepsilon \int_0^1 |f(x)|\,dx.\]

At \(x = 0\) and \(x = 1\), \(f'(x)\) is the two-sided derivative of \(f\) on \(\mathbb{R}\), taken to be \(0\) where it does not exist; this does not change the supremum.

public theorem_wanted exists_const_sSup_norm_le_mul_sSup_norm_deriv_add_mul_integral :
    ∀ ε > 0, ∃ Cε > 0, ∀ f : ℝ → ℝ,
      ContDiffOn ℝ 1 f (Set.Icc (0 : ℝ) 1) →
      sSup (Set.image (fun x => ‖f x‖) (Set.Icc (0 : ℝ) 1))
        ≤ ε * sSup (Set.image (fun x => ‖deriv f x‖) (Set.Icc (0 : ℝ) 1))
            + Cε * ∫ x in (0 : ℝ)..1, ‖f x‖

Sources

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

TheoremSup-norm bound by the \(H^1\) energy for functions vanishing at both ends#●ready to prove

Let \(\alpha \le \beta\) be real numbers and let \(f : \mathbb{R} \to \mathbb{R}\) be continuously differentiable on \([\alpha, \beta]\) with \(f(\alpha) = f(\beta) = 0\). Then

\[\Bigl(\sup_{x \in [\alpha, \beta]} |f(x)|\Bigr)^2 \le \frac{1}{2} \int_\alpha^\beta \bigl(f(x)^2 + f'(x)^2\bigr)\,dx.\]

public theorem_wanted sSup_norm_sq_le_half_integral_sq_add_deriv_sq
    {α β : ℝ} (hαβ : α ≤ β) {f : ℝ → ℝ}
    (hf : ContDiffOn ℝ 1 f (Set.Icc α β))
    (hfa : f α = 0) (hfb : f β = 0) :
    (sSup (Set.image (fun x => ‖f x‖) (Set.Icc α β))) ^ 2
      ≤ (1 / 2 : ℝ) *
          ∫ x in α..β, ((f x) ^ 2 + (deriv f x) ^ 2)

Sources

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

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.