The one-dimensional energy estimate for traces

A compactly supported C¹ real function has its squared value at the endpoint of a half-line bounded by the integral of its value and derivative squared on that half-line. Integrating this estimate over the transverse variables supplies the flat-boundary H¹ trace inequality.

The estimate follows the fundamental-theorem-of-calculus proof of the trace theorem in L. C. Evans, Partial Differential Equations, Chapter 5, §5.5.

theorem TauCeti.sq_le_integral_Ioi_sq_add_deriv_sq {g : ℝ → ℝ} (hg : ContDiff ℝ 1 g) (hs : HasCompactSupport g) (a : ℝ) : g a ^ 2 ≤ ∫ (t : ℝ) in Set.Ioi a, g t ^ 2 + deriv g t ^ 2

The endpoint value is controlled by the H¹ energy on the right half-line.

theorem TauCeti.sq_le_integral_sq_add_deriv_sq {g : ℝ → ℝ} (hg : ContDiff ℝ 1 g) (hs : HasCompactSupport g) (a : ℝ) : g a ^ 2 ≤ ∫ (t : ℝ), g t ^ 2 + deriv g t ^ 2

A point value is bounded by the whole-line H¹ energy.