Wiener–Lévy theorem

wiener_levy_analytic_calculus

Submitter: Kim Morrison.

Notes: The Wiener–Lévy theorem, the analytic functional calculus for the Wiener algebra: if f lies in the Wiener algebra (`InWienerAlgebra f := Summable (fourierCoeff f)`) and φ is complex-analytic on an open neighbourhood U of the range of f, then the composition φ ∘ f again lies in the Wiener algebra. Generalizes Wiener's 1/f theorem (take φ(z) = 1/z). mathlib has the additive circle, `fourier`, `fourierCoeff`, and `hasSum_fourier_series_of_summable`, but not the Wiener algebra or its functional calculus.

Source: P. Lévy, Sur la convergence absolue des séries de Fourier, Compositio Math. 1 (1935), 1-14; N. Wiener, Tauberian theorems, Ann. of Math. 33 (1932), 1-100. Listed as §226 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Knill, §226.

Informal solution: This is the holomorphic functional calculus in the commutative Banach algebra A(T). Since the Gelfand spectrum of A(T) is the circle (Wiener's lemma), the range of f as an algebra element equals its pointwise range, which lies in U. For φ analytic on U, define φ(f) by the Cauchy integral φ(f) = (1/2πi) ∮_Γ φ(z) (z - f)⁻¹ dz over a contour Γ in U enclosing the range of f; each resolvent (z - f)⁻¹ exists in A(T) by Wiener's lemma, the integral converges in the Banach algebra norm, and the result agrees pointwise with φ ∘ f, hence has summable Fourier coefficients.

theorem declaration uses `sorry`wiener_levy_analytic_calculus (f : C(AddCircle T, ℂ))
    (φ : ℂ → ℂ) (U : Set ℂ) (hf : LeanEval.Analysis.WienerLevy.InWienerAlgebra f)
    (hU : IsOpen U) (hrange : range f ⊆ U)
    (hφ : AnalyticOnNhd ℂ φ U) :
    ∃ g : C(AddCircle T, ℂ),
      (∀ x, g x = φ (f x)) ∧ LeanEval.Analysis.WienerLevy.InWienerAlgebra g := byT:ℝinst✝:Fact (0 < T)f:C(AddCircle T, ℂ)φ:ℂ → ℂU:Set ℂhf:InWienerAlgebra fhU:IsOpen Uhrange:range ⇑f ⊆ Uhφ:AnalyticOnNhd ℂ φ U⊢ ∃ g, (∀ (x : AddCircle T), g x = φ (f x)) ∧ InWienerAlgebra g
  sorryAll goals completed! 🐙

Solved by

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 22, 2026

• @GanjinZero with Seed Prover (ByteDance) on Jun 24, 2026