Absolutely convergent Fourier series

TheoremContinuous functions are square-integrable on one period#✓fully proved

A continuous function on ℝ is square-integrable on one period.

theorem memLp_of_continuousOn_Ioc {T : ℝ} {g : ℝ → ℂ}
    (hg : Continuous g) : MemLp g 2 (volume.restrict (Set.Ioc 0 T))

Used by 1

Used byFourier coefficients of a C¹ periodic function are absolutely summable

DefinitionLift of a periodic continuous function to the circle#✓fully proved

A T-periodic continuous function descends to a continuous function on the circle AddCircle T, via AddCircle.liftIoc.

noncomputable def liftPeriodicContinuousMap {T : ℝ} [hT' : Fact (0 < T)]
    {f : ℝ → ℂ}
    (hper : Function.Periodic f T) (hfcont : Continuous f) : C(AddCircle T, ℂ) :=
  ⟨AddCircle.liftIoc T 0 f,
    AddCircle.liftIoc_continuous (hper 0).symm hfcont.continuousOn⟩

Used by 4

Used byFourier coefficients of the lifted periodic function · Uniform convergence: · Pointwise convergence on one period · Lifted periodic function agrees with the original on a period

TheoremLifted periodic function agrees with the original on a period#✓fully proved

The descended function agrees with f on the period (0, T].

theorem liftPeriodicContinuousMap_apply {T : ℝ} [hT' : Fact (0 < T)]
    {f : ℝ → ℂ}
    (hper : Function.Periodic f T) (hfcont : Continuous f) {x : ℝ}
    (hx : x ∈ Set.Ioc 0 T) :
    liftPeriodicContinuousMap hper hfcont (x : AddCircle T) = f x

Uses 1 · Used by 1

Statement usesLift of a periodic continuous function to the circle

Used byPointwise convergence on one period

TheoremFourier coefficients on \((0, 0+T)\) equal those on \((0, T)\)#✓fully proved

The interval coefficients on (0, 0 + T] agree with those on (0, T]; this bridges Mathlib's fourierCoeff_liftIoc_eq, which is stated on (a, a + T].

theorem fourierCoeffOn_zero_add {T : ℝ} [hT' : Fact (0 < T)] {f : ℝ → ℂ} (hT : 0 < T) :
    fourierCoeffOn (lt_add_of_pos_right (0 : ℝ) (Fact.out : (0 : ℝ) < T)) f =
      fourierCoeffOn hT f

Used by 1

Used byFourier coefficients of the lifted periodic function

TheoremFourier coefficients of the lifted periodic function#✓fully proved

The Fourier coefficients of the descended function are the interval coefficients fourierCoeffOn.

theorem fourierCoeff_liftPeriodicContinuousMap {T : ℝ} (hT : 0 < T) [hT' : Fact (0 < T)]
    {f : ℝ → ℂ}
    (hper : Function.Periodic f T) (hfcont : Continuous f) (n : ℤ) :
    fourierCoeff (liftPeriodicContinuousMap hper hfcont) n = fourierCoeffOn hT f n

Uses 2 · Used by 1

Statement usesLift of a periodic continuous function to the circle

Proof usesFourier coefficients on \((0, 0+T)\) equal those on \((0, T)\)

Used byUniform convergence:

TheoremFourier coefficient bounded by the sup norm on a period#✓fully proved

A Fourier coefficient bounded by the sup norm on one period.

theorem norm_fourierCoeffOn_le_of_bound {a b : ℝ} (hab : a < b) {f : ℝ → ℂ} {C : ℝ}
    (hC : ∀ x ∈ Set.Icc a b, ‖f x‖ ≤ C) (n : ℤ) :
    ‖fourierCoeffOn hab f n‖ ≤ max C 0

TheoremCoefficient identity for a C¹ periodic function#✓fully proved

For n ≠ 0, ĉₙ(f) = (T / (2π i n)) · ĉₙ(f'). The boundary term in integration by parts vanishes by periodicity.

theorem fourierCoeffOn_eq_of_hasDerivAt {T : ℝ} (hT : 0 < T) {f f' : ℝ → ℂ}
    (hper : Function.Periodic f T)
    (hderiv : ∀ x, HasDerivAt f (f' x) x)
    (hf' : IntervalIntegrable f' volume 0 T)
    {n : ℤ} (hn : n ≠ 0) :
    fourierCoeffOn hT f n =
      (T / (2 * Real.pi * Complex.I * n)) * fourierCoeffOn hT f' n

Used by 1

Used byNorm form of the coefficient identity

TheoremNorm form of the coefficient identity#✓fully proved

Norm form of the coefficient identity.

theorem norm_fourierCoeffOn_eq_of_hasDerivAt {T : ℝ} (hT : 0 < T) {f f' : ℝ → ℂ}
    (hper : Function.Periodic f T)
    (hderiv : ∀ x, HasDerivAt f (f' x) x)
    (hf' : IntervalIntegrable f' volume 0 T)
    {n : ℤ} (hn : n ≠ 0) :
    ‖fourierCoeffOn hT f n‖ =
      (T / (2 * Real.pi * |(n : ℝ)|)) * ‖fourierCoeffOn hT f' n‖

Uses 1 · Used by 2

Proof usesCoefficient identity for a C¹ periodic function

Used byFourier coefficients of a C¹ periodic function are absolutely summable · Decay rate:

TheoremFourier coefficients of a C¹ periodic function are absolutely summable#✓fully proved

Fourier coefficients of a C¹ periodic function are absolutely summable.

theorem summable_fourierCoeffOn_of_hasDerivAt {T : ℝ} (hT : 0 < T) {f f' : ℝ → ℂ}
    (hper : Function.Periodic f T)
    (hderiv : ∀ x, HasDerivAt f (f' x) x)
    (hf'cont : Continuous f') :
    Summable (fourierCoeffOn hT f)

Uses 2 · Used by 1

Proof usesContinuous functions are square-integrable on one period · Norm form of the coefficient identity

Used byUniform convergence:

TheoremDecay rate:#✓fully proved

n · ‖ĉₙ(f)‖ → 0 along the cofinite filter.

theorem tendsto_mul_norm_fourierCoeffOn_of_hasDerivAt {T : ℝ} (hT : 0 < T)
    {f f' : ℝ → ℂ}
    (hper : Function.Periodic f T)
    (hderiv : ∀ x, HasDerivAt f (f' x) x)
    (hf'cont : Continuous f') :
    Filter.Tendsto (fun n : ℤ => (n : ℝ) * ‖fourierCoeffOn hT f n‖)
      Filter.cofinite (nhds 0)

Uses 2

Proof usesNorm form of the coefficient identity · Riemann–Lebesgue lemma on an interval

TheoremUniform convergence:#✓fully proved

The Fourier series of a C¹ periodic function converges uniformly (in C(AddCircle T, ℂ)) to f on the circle.

theorem hasSum_fourier_series_of_hasDerivAt {T : ℝ} (hT : 0 < T) [hT' : Fact (0 < T)]
    {f f' : ℝ → ℂ}
    (hper : Function.Periodic f T) (hfcont : Continuous f)
    (hderiv : ∀ x, HasDerivAt f (f' x) x)
    (hf'cont : Continuous f') :
    HasSum (fun n : ℤ => fourierCoeffOn hT f n • (fourier n : C(AddCircle T, ℂ)))
      (liftPeriodicContinuousMap hper hfcont)

Uses 3 · Used by 1

Statement usesLift of a periodic continuous function to the circle

Proof usesFourier coefficients of the lifted periodic function · Fourier coefficients of a C¹ periodic function are absolutely summable

Used byPointwise convergence on one period

TheoremPointwise convergence on one period#✓fully proved

Pointwise convergence on one period.

theorem hasSum_fourier_series_of_hasDerivAt_apply {T : ℝ} (hT : 0 < T)
    [hT' : Fact (0 < T)] {f f' : ℝ → ℂ}
    (hper : Function.Periodic f T) (hfcont : Continuous f)
    (hderiv : ∀ x, HasDerivAt f (f' x) x)
    (hf'cont : Continuous f') {x : ℝ} (hx : x ∈ Set.Ioc 0 T) :
    HasSum (fun n : ℤ => fourierCoeffOn hT f n • (fourier n (x : AddCircle T) : ℂ))
      (f x)

Uses 3

Proof usesUniform convergence: · Lift of a periodic continuous function to the circle · Lifted periodic function agrees with the original on a period

DefinitionWiener algebra on the circle#✓fully proved

Let \(T > 0\). A continuous function \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) lies in the Wiener algebra when the family of its Fourier coefficients \(\hat f(n) = \frac{1}{T} \int_0^T f(x) e^{-2\pi i n x / T} \, dx\), \(n \in \mathbb{Z}\), is summable in \(\mathbb{C}\).

For complex families, summability is equivalent to \(\sum_{n \in \mathbb{Z}} |\hat f(n)| < \infty\), so these are the functions with absolutely convergent Fourier series.

def InWienerAlgebra (f : C(AddCircle T, ℂ)) : Prop :=
  Summable (fourierCoeff f)

Used by 1

Used byWiener–Lévy theorem

TheoremWiener–Lévy theorem#●ready to prove

Let \(T > 0\), and let \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) be a continuous function in the Wiener algebra. Let \(U \subseteq \mathbb{C}\) be an open set containing the range of \(f\), and let \(\varphi : \mathbb{C} \to \mathbb{C}\) be analytic at every point of \(U\). Then there is a continuous function \(g : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) with \(g(x) = \varphi(f(x))\) for every \(x\), and \(g\) lies in the Wiener algebra.

public theorem_wanted 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

Sources

• 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. Problem wiener_levy_analytic_calculus of the lean-eval benchmark.

Uses 1

Statement usesWiener algebra on the circle

DefinitionFunctions with absolutely convergent Fourier series#✓fully proved

Let \(T > 0\). A continuous function \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) lies in the Wiener algebra when the family of its Fourier coefficients \(\hat f(n) = \frac{1}{T} \int_0^T f(x) e^{-2\pi i n x / T} \, dx\), \(n \in \mathbb{Z}\), is summable in \(\mathbb{C}\).

For complex families, summability is equivalent to \(\sum_{n \in \mathbb{Z}} |\hat f(n)| < \infty\).

def InWienerAlgebra (f : C(AddCircle T, ℂ)) : Prop :=
  Summable (fourierCoeff f)

Used by 1

Used byWiener's 1/f theorem

TheoremWiener's 1/f theorem#●ready to prove

Let \(T > 0\), and let \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) be a continuous function in the Wiener algebra with \(f(x) \ne 0\) for every \(x\). Then there is a continuous function \(g : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) with \(g(x) = f(x)^{-1}\) for every \(x\), and \(g\) lies in the Wiener algebra.

public theorem_wanted wiener_inverse_closed (f : C(AddCircle T, ℂ))
    (hf : InWienerAlgebra f) (hzero : ∀ x, f x ≠ 0) :
    ∃ g : C(AddCircle T, ℂ),
      (∀ x, g x = (f x)⁻¹) ∧ InWienerAlgebra g

Sources

• 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. Problem wiener_inverse_closed of the lean-eval benchmark.

Uses 1

Statement usesFunctions with absolutely convergent Fourier series

14 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.