The du Bois-Reymond lemma on an interval (ported from TauCeti)

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 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.

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 - c) = 0 for c = ∫ ρ • f. Hence f = c almost everywhere on the interval, and everywhere by continuity.

Main declarations

• 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.
• exists_eqOn_const_Ioo_of_integral_deriv_smul_eq_zero: the du Bois-Reymond lemma.

Provenance

Pool port: imports relocated under LeanPool.ViscositySolutionTheory; original mathematical namespaces and copyright retained; checked with Lean/Mathlib v4.34.0.

• Upstream: TauCeti, https://github.com/TauCetiProject/TauCeti
• Path: TauCeti/Analysis/Distribution/DuBoisReymond.lean
• Commit: 91f66a0514e6523efdccddb9e35fb82c96dd6405 (2026-09-24)
• License: Apache-2.0. Upstream NOTICE: none.
• Upstream notice: Copyright (c) 2026 The Tau Ceti contributors. All rights reserved.; upstream authors: The Tau Ceti contributors.
• Extent: the whole file (verbatim up to naming).
• Changes: ported from Lean v4.34.0-rc2 to Lean/Mathlib v4.30.0; module/public import removed; namespace TauCeti → ViscositySolns.Analysis; the two theorems are no longer stated in the root namespaces ContDiff/ContinuousOn.

theorem ViscositySolns.Analysis.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 ViscositySolns.Analysis.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.