Poincaré inequality on an interval for a curve vanishing at the left endpoint, with a skew-twisted derivative

Proved

FiniteEnergyPlane.integral_norm_sq_le_of_skew

by Mazecto · Oct 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

inequalitiesinner-product-spacesreal-analysis

Let $E$ be a real inner product space and $T:E\to E$ a bounded linear operator that is skew in the sense $\langle v,Tv\rangle=0$ for all $v\in E$ . Let $w:\mathbb{R}\to E$ be differentiable with continuous derivative $w'$ , and suppose $w(x_0)=0$ . Then for every $L>0$ ,

\int_{x_0}^{x_0+L}\|w(t)\|^2\,dt\ \le\ 4L^2\int_{x_0}^{x_0+L}\big\|w'(t)-T\,w(t)\big\|^2\,dt .

For $T=0$ this is a one-dimensional Poincaré inequality for functions vanishing at an endpoint. The twisted form allows $w'$ to be replaced by $w'-Tw$ for any skew $T$ , for instance $T=aJ_0$ with the standard complex structure $J_0$ on $\mathbb{R}^{2n}$ . It is a reusable estimate for loops with controlled twisted derivative, as in the spectral theory of asymptotic operators (C. Wendl, Lectures on Symplectic Field Theory, 2026 notes, Section 3.5).

Formalization Note $T$ is a continuous linear map E →L[ℝ] E with ∀ v, ⟪v, T v⟫ = 0. The derivative is supplied as a continuous w' with HasDerivAt w (w' t) t for all t. The integrals are interval integrals over x₀..x₀ + L.

Preamble

import Mathlib

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory
open scoped RealInnerProductSpace

/-- Let `T` be a skew operator (`⟪v, T v⟫ = 0`) on a real inner product space and let `w` be a
`C¹` curve with `w(x₀) = 0`. Then on `[x₀, x₀ + L]`,
`∫ ‖w‖² ≤ 4 L² ∫ ‖w' - T w‖²`. -/
theorem integral_norm_sq_le_of_skew {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (T : E →L[ℝ] E) (hT : ∀ v, ⟪v, T v⟫ = 0) (w w' : ℝ → E)
    (hw : ∀ t, HasDerivAt w (w' t) t) (hw' : Continuous w') (x₀ L : ℝ) (hL : 0 < L)
    (h0 : w x₀ = 0) :
    ∫ t in x₀..x₀ + L, ‖w t‖ ^ 2 ≤ 4 * L ^ 2 * ∫ t in x₀..x₀ + L, ‖w' t - T (w t)‖ ^ 2 := by
  sorry

end FiniteEnergyPlane

Source

Elementary; used for the uniform spectral gaps of asymptotic operators in C. Wendl, Lectures on Symplectic Field Theory (2026 notes), Section 3.5

View graph