Translation-invariant operator
TranslationInvariantdef
An operator on functions is translation invariant when it commutes with shifting the argument. On the circle these are exactly the Fourier multipliers, which is why the definition sits at the entrance to harmonic analysis.
def TranslationInvariant {G E : Type*} [Add G] (T : (G → E) → (G → E)) : Prop :=
∀ (f : G → E) (g : G), T (fun x => f (x + g)) = fun x => T f (x + g)From Mathlib
import Conjectura.Defs.Mathematics.Analysis.HarmonicAnalysis.TranslationInvariant · maintainer — open · raw source
Copyright (c) 2026 The Conjectura Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Conjectura Authors