The du Bois-Reymond lemma on an interval

A function on an open interval whose distributional derivative vanishes is constant. Concretely, if f : ℝ → F is continuous on Ioo a b and

∫ x, deriv ψ x • f x = 0

for every smooth ψ : ℝ → ℝ with tsupport ψ ⊆ Ioo a b, then f is constant on Ioo a b. This is the one-variable du Bois-Reymond lemma, the derivative form of the fundamental lemma of the calculus of variations, whose zeroth-order form is Mathlib's IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero.

The reduction to the zeroth-order lemma is the classical one. Fix a test function ρ on the interval with total integral 1. For a test function g, the function g - (∫ g) ρ has total integral zero, so its primitive ψ is again a test function on the interval, with deriv ψ = g - (∫ g) ρ; the hypothesis applied to ψ gives ∫ g • f = (∫ g) • ∫ ρ • f, that is ∫ g • (f - c) = 0 for the constant c = ∫ ρ • f. Hence f = c almost everywhere on the interval, and everywhere by continuity.

The one-sided version says that a continuous real function whose distributional derivative is nonnegative is monotone: if ∫ x, deriv ψ x * f x ≤ 0 for every nonnegative test function ψ on the interval, then f is monotone there. For x ≤ y in the interval, take ψ to be the difference of the primitives of two copies of a narrow bump of integral one, centred at x and at y; then ψ ≥ 0, and ∫ ψ' f is the difference of the averages of f against the two bumps, which are close to f x and f y by continuity.

Main declarations

• ContDiff.exists_contDiff_deriv_eq_of_integral_eq_zero: the primitive of a test function on an interval with total integral zero is a test function on the interval.
• ContinuousOn.exists_eqOn_const_Ioo_of_integral_deriv_smul_eq_zero: the du Bois-Reymond lemma.
• ContinuousOn.monotoneOn_of_integral_deriv_mul_nonpos: a continuous function with nonnegative distributional derivative is monotone.

theorem ContDiff.exists_contDiff_deriv_eq_of_integral_eq_zero {a b : ℝ} {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : tsupport φ ⊆ Set.Ioo a b) (hint : ∫ (x : ℝ), φ x = 0) : ∃ (ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ tsupport ψ ⊆ Set.Ioo a b ∧ deriv ψ = φ

The primitive of a mean-zero test function is a test function. If φ : ℝ → ℝ is smooth with tsupport φ ⊆ Ioo a b and ∫ φ = 0, then φ is the derivative of a smooth compactly supported function ψ with tsupport ψ ⊆ Ioo a b.

theorem ContinuousOn.exists_eqOn_const_Ioo_of_integral_deriv_smul_eq_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b : ℝ} {f : ℝ → F} (hf : ContinuousOn f (Set.Ioo a b)) (h : ∀ (ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → tsupport ψ ⊆ Set.Ioo a b → ∫ (x : ℝ), deriv ψ x • f x = 0) : ∃ (c : F), Set.EqOn f (fun (x : ℝ) => c) (Set.Ioo a b)

The du Bois-Reymond lemma. A function continuous on an open interval whose pairing with the derivative of every test function on the interval vanishes, ∫ x, deriv ψ x • f x = 0, is constant on the interval.

theorem ContinuousOn.monotoneOn_of_integral_deriv_mul_nonpos {a b : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Ioo a b)) (h : ∀ (ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → tsupport ψ ⊆ Set.Ioo a b → (∀ (x : ℝ), 0 ≤ ψ x) → ∫ (x : ℝ), deriv ψ x * f x ≤ 0) : MonotoneOn f (Set.Ioo a b)

The monotone du Bois-Reymond lemma. A real function continuous on an open interval whose distributional derivative is nonnegative, in the sense that ∫ x, deriv ψ x * f x ≤ 0 for every nonnegative test function ψ on the interval, is monotone on the interval.