Integral Of An Integrable Weak Derivative

This statement gives the cutoff lemma used for equation (2.1) and Lemma 2.7 of Letwin (arXiv:2607.24164v1).

Let f and g be real-valued functions on $E=\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin} n)$, and let v∈E. Assume g is a weak directional derivative of f along v, written $\partial_v f=g$, and assume both f and g are integrable with respect to Lebesgue volume. Then

This is a global zero-mean property for an integrable weak derivative and is reusable as a cutoff argument in weak integration by parts.

Formalization Note No positivity, smoothness, or nonzero-direction assumption is included; the assertion applies to every natural number n and every direction v.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem integral_eq_zero_of_integrable_weak_derivative {n : ℕ}
    {f g : EuclideanSpace ℝ (Fin n) → ℝ} {v : EuclideanSpace ℝ (Fin n)}
    (hweak : HasWeakDerivAlong f g v)
    (hf : Integrable f volume) (hg : Integrable g volume) :
    (∫ x, g x ∂volume) = 0

Module navigation

Module: Analysis/WeakDerivative/Calculus.

Definition modules: Analysis/WeakDerivative/Basic.

Previous: integral_compact_flux_eq_neg_forcing_of_global_bounded_weak_test.

Source excerpt, lines 1494–1498 · Frozen source 408915f.