Wiener–Lévy theorem

wiener_levy_analytic_calculus — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Wiener–Lévy theorem.** If `φ` is complex-analytic on a neighbourhood of
the range of a Wiener-algebra function `f`, then the composed function
`φ ∘ f` is again in the Wiener algebra. -/
theorem wiener_levy_analytic_calculus (f : C(AddCircle T, ℂ))
    (φ : ℂ → ℂ) (U : Set ℂ) (hf : InWienerAlgebra f)
    (hU : IsOpen U) (hrange : range f ⊆ U)
    (hφ : AnalyticOnNhd ℂ φ U) :
    ∃ g : C(AddCircle T, ℂ),
      (∀ x, g x = φ (f x)) ∧ InWienerAlgebra g := by
  sorry

Informal solution sketch

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.

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.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: wiener_levy_analytic_calculus
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.