Translation preserves $L^q$ membership and norm on restricted measures

Proved

JHolomorphic.memLp_comp_add_right

by Mazecto · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

sobolev-spacesweak-derivatives

Let $E$ be a normed group, $\mu$ a translation-invariant measure on $\mathbb{C}$ , $S\subseteq\mathbb{C}$ measurable, $q\in[0,\infty]$ , and $a\in\mathbb{C}$ . If $g\in L^q(S,\mu)$ , then $g(\cdot+a)\in L^q(S-a,\mu)$ and

\|g(\cdot+a)\|_{L^q(S-a,\mu)}=\|g\|_{L^q(S,\mu)},\qquad S-a=\{z: z+a\in S\}.

Formalization Note $L^q$ membership and norms are MemLp and eLpNorm for the restricted measures μ.restrict ((· + a) ⁻¹' S) and μ.restrict S; translation invariance is μ.IsAddRightInvariant.

Preamble

import Definitions.Def_JHolomorphic_Setting
import Mathlib.MeasureTheory.Group.Measure

Formal statement

namespace JHolomorphic

open MeasureTheory Metric

/-- For a translation-invariant measure `μ` on `ℂ` and a measurable set `S`, if `g ∈ L^q(S)` then
`g(· + a) ∈ L^q(S - a)`, with the same norm. -/
theorem memLp_comp_add_right {E : Type*} [NormedAddCommGroup E] {μ : Measure ℂ}
    [μ.IsAddRightInvariant] {q : ENNReal} {g : ℂ → E} {S : Set ℂ} (hS : MeasurableSet S) (a : ℂ)
    (hg : MemLp g q (μ.restrict S)) :
    MemLp (fun z => g (z + a)) q (μ.restrict ((· + a) ⁻¹' S)) ∧
      eLpNorm (fun z => g (z + a)) q (μ.restrict ((· + a) ⁻¹' S)) = eLpNorm g q (μ.restrict S) := by
  sorry

end JHolomorphic

Source

Standard (weak derivatives and Lebesgue spaces).

View graph

Translation preserves LqL^qLq membership and norm on restricted measures

Translation preserves $L^q$ membership and norm on restricted measures