Translation Invariance From Vanishing Weak Derivatives

This is a distributional translation-invariance statement for a locally integrable function.

Let $V$ be a finite-dimensional real inner-product normed additive group equipped with its Borel measurable structure and a second-countable topology. Let $m$ be an additive Haar measure on $V$, and let $h:V\to\mathbb R$ be locally integrable with respect to $m$. Assume that for every smooth compactly supported test function $\varphi:V\to\mathbb R$ and every direction $w\in V$,

Then, for every translation vector $v\in V$, $h$ is invariant under translation by $v$ almost everywhere:

The Lean declaration is ae_add_eq_of_integral_mul_fderiv_eq_zero_readable; the values are real, and the conclusion is an a.e. equality for each fixed translation vector. This is an auxiliary weak-gradient result and does not itself assert that $h$ is almost everywhere constant.

Original Lean declaration header

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

theorem ae_add_eq_of_integral_mul_fderiv_eq_zero {h : V → ℝ} (hh : LocallyIntegrable h m)
    (h0 : ∀ φ : V → ℝ, ContDiff ℝ ∞ φ → HasCompactSupport φ → ∀ w : V,
      ∫ x, h x * fderiv ℝ φ x w ∂m = 0)
    (v : V) :
    ∀ᵐ x ∂m, h (x + v) = h x

Module navigation

Module: Energy/Euclidean/ZeroGradient.

Supporting theorems: integral_mul_sub_translate_eq_zero, locallyIntegrable_comp_add_right.

Previous: locallyIntegrable_comp_add_right · Next: exists_ae_eq_const_of_measurable_of_forall_ae_add_eq.

Source excerpt, lines 277–281 · Frozen source 408915f.