Translation-invariant operator

Conjectura.Defs.Mathematics.Analysis.HarmonicAnalysis.TranslationInvariant

/-
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
-/
import Mathlib.Algebra.Group.Defs

/-! # Translation-invariant operator -/

namespace Conjectura.HarmonicAnalysis

/-- 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)

end Conjectura.HarmonicAnalysis