Almost-Everywhere Constancy From Translation Invariance

Proved

FunctionalInequalities.Energy.Euclidean.exists_ae_eq_const_of_measurable_of_forall_ae_add_eq_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a measurable translation-invariance criterion for almost-everywhere constancy.

Let $V$ be a finite-dimensional real inner-product normed additive group with its Borel measurable structure, and let $m$ be an additive Haar measure. For a measurable function $g:V\to\mathbb R$ , assume that every translation preserves $g$ almost everywhere:

\forall v\in V,\qquad g(x+v)=g(x)\quad\text{for $m$-almost every }x.

Then there exists a constant $c\in\mathbb R$ such that

g(x)=c\quad\text{for $m$-almost every }x.

The Lean declaration is exists_ae_eq_const_of_measurable_of_forall_ae_add_eq_readable. It is a reusable measure-theoretic auxiliary lemma; the conclusion is existential and only asserts equality almost everywhere.

Original Lean declaration header

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

theorem exists_ae_eq_const_of_measurable_of_forall_ae_add_eq {g : V → ℝ} (hg : Measurable g)
    (htr : ∀ v : V, ∀ᵐ x ∂m, g (x + v) = g x) :
    ∃ c : ℝ, ∀ᵐ x ∂m, g x = c

Module navigation

Module: Energy/Euclidean/ZeroGradient.

Previous: ae_add_eq_of_integral_mul_fderiv_eq_zero.

Source excerpt, lines 342–344 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_ZeroGradient

universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
variable [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure]

Formal statement


theorem FunctionalInequalities.Energy.Euclidean.exists_ae_eq_const_of_measurable_of_forall_ae_add_eq_readable {g : V → ℝ} (hg : Measurable g)
    (htr : ∀ v : V, ∀ᵐ x ∂m, g (x + v) = g x) :
    ∃ c : ℝ, ∀ᵐ x ∂m, g x = c := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/Euclidean/ZeroGradient.lean#L340-L370 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.Euclidean.ZeroGradient`, declaration `FunctionalInequalities.Energy.Euclidean.exists_ae_eq_const_of_measurable_of_forall_ae_add_eq`; the repository is private at upload time).

View graph