Local Integrability Under Haar Translation
ProvedFunctionalInequalities.Energy.Euclidean.locallyIntegrable_comp_add_right_readableThis states stability of local integrability under translation.
Let be a finite-dimensional real inner-product space with its Borel measurable structure, let be an additive Haar measure on , and let be locally integrable with respect to . For every , the translated function
is also locally integrable with respect to .
This is a measure-theoretic auxiliary fact used when comparing a function with its translates in weak-gradient arguments.
Formalization Note The declaration omits the second-countable-topology assumption; the additive Haar-measure instance is explicit.
Original Lean declaration header
Within namespace FunctionalInequalities.Energy.Euclidean. Shown in its original module context. Proof omitted.
theorem locallyIntegrable_comp_add_right {h : V → ℝ} (hh : LocallyIntegrable h m) (v : V) :
LocallyIntegrable (fun x => h (x + v)) m
Module navigation
Module: Energy/Euclidean/ZeroGradient.
Previous: integral_mul_sub_translate_eq_zero · Next: ae_add_eq_of_integral_mul_fderiv_eq_zero.
Source excerpt, lines 252–253 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_ZeroGradient
open MeasureTheory Filter Topology
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]
omit [SecondCountableTopology V]
theorem FunctionalInequalities.Energy.Euclidean.locallyIntegrable_comp_add_right_readable {h : V → ℝ} (hh : LocallyIntegrable h m) (v : V) :
LocallyIntegrable (fun x => h (x + v)) m := by sorry