Multiplication operators on the Sobolev spaces of the circle

On Fourier coefficients, multiplying a function on the circle by the monomial e^{imθ} shifts the coefficients by m, and multiplying by g = ∑ₘ gₘ e^{imθ} convolves them with (gₘ). This file constructs these operators on the Fourier-coefficient Sobolev spaces H^s of TauCeti/Analysis/Sobolev/Circle/Basic.lean, for every real order s, including fractional orders, and negative orders where elements of H^s may be distributions rather than functions.

By Peetre's inequality (CircleSobolev.weight_add_le), the shift by m has norm at most (1 + |m|) ^ |s| on H^s. The multiplication operator by the coefficient sequence g is then the operator-norm convergent series ∑ₘ gₘ • shift m, as soon as ∑ₘ (1 + |m|) ^ |s| ‖gₘ‖ < ∞. A smooth function on the circle has rapidly decaying Fourier coefficients, so it satisfies this for every s: multiplication by a smooth function is a bounded operator on every H^s, and it is invertible when the function vanishes nowhere. Such multipliers are needed to patch boundary estimates with smooth partitions of unity and cutoffs.

Main definitions

• TauCeti.CircleSobolev.shift m: multiplication by e^{imθ}, shifting the Fourier coefficients by m.
• TauCeti.CircleSobolev.mulFourierSeries g: the series ∑ₘ g m • shift m. When ∑ₘ (1 + |m|) ^ |s| ‖g m‖ < ∞ and E is complete, this is multiplication by the function with Fourier coefficients g; when the series does not converge it is the junk value 0.
• TauCeti.CircleSobolev.mulFourierSeriesEquiv: for a smooth nowhere-vanishing function f, multiplication by f as a continuous linear automorphism of H^s.
• TauCeti.CircleSobolev.multiplicationOperator a: multiplication by an essentially bounded function a on H⁰ = L², for instance by a continuous function, which need not satisfy the summability hypothesis of mulFourierSeries.

Main statements

• TauCeti.CircleSobolev.norm_shift_le: ‖shift m a‖ ≤ (1 + |m|) ^ |s| ‖a‖.
• TauCeti.CircleSobolev.opNorm_mulFourierSeries_le: the operator norm of mulFourierSeries g on H^s is at most ∑ₘ (1 + |m|) ^ |s| ‖g m‖.
• TauCeti.CircleSobolev.coeff_mulFourierSeries: the Fourier coefficients of mulFourierSeries g a are the convolution ∑ₘ g m • a.coeff (n - m).
• TauCeti.CircleSobolev.mulFourierSeries_add, TauCeti.CircleSobolev.mulFourierSeries_smul, TauCeti.CircleSobolev.mulFourierSeries_single: mulFourierSeries g is linear in g, and mulFourierSeries (Pi.single m c) = c • shift m.
• TauCeti.CircleSobolev.toContinuousMap_mulFourierSeries_fourierCoeff: for s > 1/2, the operator mulFourierSeries (fourierCoeff f) is pointwise multiplication by f on continuous representatives.
• TauCeti.CircleSobolev.summable_weight_mul_norm_fourierCoeff: a C^k function on the circle satisfies the summability hypothesis of mulFourierSeries on H^s for |s| < k - 1, so a smooth function satisfies it for every order (TauCeti.CircleSobolev.summable_weight_mul_norm_fourierCoeff_of_contDiff).
• TauCeti.CircleSobolev.mulFourierSeries_fourierCoeff_comp: for smooth f and g, multiplication by f after multiplication by g is multiplication by f * g.
• TauCeti.CircleSobolev.toLpₗᵢ_multiplicationOperator_ae and TauCeti.CircleSobolev.norm_multiplicationOperator_apply_le: on H⁰, multiplicationOperator a is pointwise multiplication by a almost everywhere, and ‖a · u‖ ≤ ‖a‖∞ ‖u‖.
• TauCeti.CircleSobolev.multiplicationOperator_add, TauCeti.CircleSobolev.multiplicationOperator_smul, TauCeti.CircleSobolev.multiplicationOperator_comp_multiplicationOperator: on H⁰, multiplicationOperator a is linear in a, and composing two of them multiplies the symbols.
• TauCeti.CircleSobolev.mulFourierSeries_fourierCoeff_eq_multiplicationOperator: on H⁰, the two multiplication operators by a smooth function agree.

References

• M. E. Taylor, Partial Differential Equations I, Chapter 3 (Sobolev spaces on the torus via Fourier series, and multiplication by smooth functions).

Shifts of the Fourier coefficients

noncomputable def TauCeti.CircleSobolev.shift {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (m : ℤ) : CircleSobolev s E →L[ℂ] CircleSobolev s E

Multiplication by the Fourier monomial e^{imθ}, which shifts the Fourier coefficients by m.

@[simp]

theorem TauCeti.CircleSobolev.coeff_shift {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (m : ℤ) (a : CircleSobolev s E) (n : ℤ) : ((shift m) a).coeff n = a.coeff (n - m)

theorem TauCeti.CircleSobolev.norm_shift_le {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (m : ℤ) (a : CircleSobolev s E) : ‖(shift m) a‖ ≤ weight |s| m * ‖a‖

The shift by m changes the H^s norm by at most the factor (1 + |m|) ^ |s|.

theorem TauCeti.CircleSobolev.opNorm_shift_le {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (m : ℤ) : ‖shift m‖ ≤ weight |s| m

@[simp]

theorem TauCeti.CircleSobolev.shift_zero {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : CircleSobolev s E) : (shift 0) a = a

@[simp]

theorem TauCeti.CircleSobolev.shift_shift {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (m k : ℤ) (a : CircleSobolev s E) : (shift m) ((shift k) a) = (shift (m + k)) a

@[simp]

theorem TauCeti.CircleSobolev.shift_single {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (m n : ℤ) (x : E) : (shift m) ((single n) x) = (single (m + n)) x

@[simp]

theorem TauCeti.CircleSobolev.inclusion_shift {s t : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (h : t ≤ s) (m : ℤ) (a : CircleSobolev s E) : (inclusion h) ((shift m) a) = (shift m) ((inclusion h) a)

@[simp]

theorem TauCeti.CircleSobolev.toContinuousMap_shift {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (T : ℝ) [Fact (0 < T)] [CompleteSpace E] (hs : 1 / 2 < s) (m : ℤ) (a : CircleSobolev s E) (x : AddCircle T) : ((toContinuousMap T hs) ((shift m) a)) x = (fourier m) x • ((toContinuousMap T hs) a) x

For s > 1/2, the shift by m is multiplication by e^{2πimx/T} on continuous representatives.

Multiplication operators

noncomputable def TauCeti.CircleSobolev.mulFourierSeries {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (g : ℤ → ℂ) : CircleSobolev s E →L[ℂ] CircleSobolev s E

The series ∑ₘ g m • shift m of operators on H^s. When ∑ₘ (1 + |m|) ^ |s| ‖g m‖ < ∞ and E is complete, the series converges in operator norm (hasSum_mulFourierSeries) and this is the operator of multiplication by the function with Fourier coefficients g; when the series does not converge, it is the junk value 0. This is a pointwise multiplier, not a Fourier multiplier: on coefficients it acts by convolution with g (coeff_mulFourierSeries). The summability condition holds in particular when g is the sequence of Fourier coefficients of a sufficiently smooth function (summable_weight_mul_norm_fourierCoeff).

theorem TauCeti.CircleSobolev.opNorm_mulFourierSeries_le {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : ℤ → ℂ} (hg : Summable fun (m : ℤ) => weight |s| m * ‖g m‖) : ‖mulFourierSeries g‖ ≤ ∑' (m : ℤ), weight |s| m * ‖g m‖

The operator norm of mulFourierSeries g on H^s is at most ∑ₘ (1 + |m|) ^ |s| ‖g m‖.

theorem TauCeti.CircleSobolev.mulFourierSeries_smul {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : ℤ → ℂ} (c : ℂ) : mulFourierSeries (c • g) = c • mulFourierSeries g

mulFourierSeries g is homogeneous in the coefficient sequence g.

@[simp]

theorem TauCeti.CircleSobolev.mulFourierSeries_single {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (m : ℤ) (c : ℂ) : mulFourierSeries (Pi.single m c) = c • shift m

Multiplication by the function with a single nonzero Fourier coefficient c at m is c times the shift by m.

theorem TauCeti.CircleSobolev.hasSum_mulFourierSeries {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : ℤ → ℂ} [CompleteSpace E] (hg : Summable fun (m : ℤ) => weight |s| m * ‖g m‖) : HasSum (fun (m : ℤ) => g m • shift m) (mulFourierSeries g)

The series defining mulFourierSeries g converges in operator norm when the coefficients g are summable against the weights of order |s|.

theorem TauCeti.CircleSobolev.hasSum_mulFourierSeries_apply {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : ℤ → ℂ} [CompleteSpace E] (hg : Summable fun (m : ℤ) => weight |s| m * ‖g m‖) (a : CircleSobolev s E) : HasSum (fun (m : ℤ) => g m • (shift m) a) ((mulFourierSeries g) a)

theorem TauCeti.CircleSobolev.mulFourierSeries_add {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : ℤ → ℂ} [CompleteSpace E] {g' : ℤ → ℂ} (hg : Summable fun (m : ℤ) => weight |s| m * ‖g m‖) (hg' : Summable fun (m : ℤ) => weight |s| m * ‖g' m‖) : mulFourierSeries (g + g') = mulFourierSeries g + mulFourierSeries g'

mulFourierSeries g is additive in the coefficient sequence g, for sequences summable against the weights of order |s|.

theorem TauCeti.CircleSobolev.coeff_mulFourierSeries {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : ℤ → ℂ} [CompleteSpace E] (hg : Summable fun (m : ℤ) => weight |s| m * ‖g m‖) (a : CircleSobolev s E) (n : ℤ) : ((mulFourierSeries g) a).coeff n = ∑' (m : ℤ), g m • a.coeff (n - m)

The Fourier coefficients of mulFourierSeries g a are the convolution of g with those of a.

theorem TauCeti.CircleSobolev.inclusion_mulFourierSeries {s t : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : ℤ → ℂ} [CompleteSpace E] (h : t ≤ s) (hgs : Summable fun (m : ℤ) => weight |s| m * ‖g m‖) (hgt : Summable fun (m : ℤ) => weight |t| m * ‖g m‖) (a : CircleSobolev s E) : (inclusion h) ((mulFourierSeries g) a) = (mulFourierSeries g) ((inclusion h) a)

Multiplication operators commute with the inclusions between the Sobolev spaces.

theorem TauCeti.CircleSobolev.toContinuousMap_mulFourierSeries {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {g : ℤ → ℂ} [CompleteSpace E] (T : ℝ) [Fact (0 < T)] (hs : 1 / 2 < s) (hg : Summable fun (m : ℤ) => weight |s| m * ‖g m‖) (a : CircleSobolev s E) (x : AddCircle T) : ((toContinuousMap T hs) ((mulFourierSeries g) a)) x = (∑' (m : ℤ), g m * (fourier m) x) • ((toContinuousMap T hs) a) x

For s > 1/2, mulFourierSeries g is pointwise multiplication by ∑ₘ g m e^{2πimx/T} on continuous representatives.

theorem TauCeti.CircleSobolev.toContinuousMap_mulFourierSeries_fourierCoeff {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (T : ℝ) [Fact (0 < T)] (hs : 1 / 2 < s) {f : AddCircle T → ℂ} (hfc : Continuous f) (hf : Summable fun (m : ℤ) => weight |s| m * ‖fourierCoeff f m‖) (a : CircleSobolev s E) (x : AddCircle T) : ((toContinuousMap T hs) ((mulFourierSeries (fourierCoeff f)) a)) x = f x • ((toContinuousMap T hs) a) x

For a continuous function f on the circle whose Fourier coefficients are summable against the weights of order |s|, with s > 1/2, the operator mulFourierSeries (fourierCoeff f) is pointwise multiplication by f on continuous representatives.

Multiplication by smooth functions

theorem TauCeti.CircleSobolev.summable_weight_mul_norm_fourierCoeff {T : ℝ} [Fact (0 < T)] {f : AddCircle T → ℂ} {k : ℕ} (hf : ContDiff ℝ ↑k fun (x : ℝ) => f ↑x) {r : ℝ} (hr : r + 1 < ↑k) : Summable fun (n : ℤ) => weight r n * ‖fourierCoeff f n‖

The Fourier coefficients of a C^k function on the circle are summable against the weights (1 + |n|) ^ r of every order r < k - 1. In particular, multiplication by a C^k function is bounded on H^s whenever |s| < k - 1 (opNorm_mulFourierSeries_le).

theorem TauCeti.CircleSobolev.summable_weight_mul_norm_fourierCoeff_of_contDiff {T : ℝ} [Fact (0 < T)] {f : AddCircle T → ℂ} (hf : ContDiff ℝ ↑⊤ fun (x : ℝ) => f ↑x) (r : ℝ) : Summable fun (n : ℤ) => weight r n * ‖fourierCoeff f n‖

The Fourier coefficients of a smooth function on the circle are summable against the weights (1 + |n|) ^ r of every real order r. So multiplication by a smooth function is bounded on every H^s (opNorm_mulFourierSeries_le).

theorem TauCeti.CircleSobolev.toContinuousMap_mulFourierSeries_fourierCoeff_of_contDiff {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {T : ℝ} [Fact (0 < T)] (hs : 1 / 2 < s) {f : AddCircle T → ℂ} (hf : ContDiff ℝ ↑⊤ fun (x : ℝ) => f ↑x) (a : CircleSobolev s E) (x : AddCircle T) : ((toContinuousMap T hs) ((mulFourierSeries (fourierCoeff f)) a)) x = f x • ((toContinuousMap T hs) a) x

For s > 1/2, multiplication by a smooth function f on H^s is pointwise multiplication by f on continuous representatives.

theorem TauCeti.CircleSobolev.mulFourierSeries_fourierCoeff_comp {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {T : ℝ} [Fact (0 < T)] {f g : AddCircle T → ℂ} (hf : ContDiff ℝ ↑⊤ fun (x : ℝ) => f ↑x) (hg : ContDiff ℝ ↑⊤ fun (x : ℝ) => g ↑x) : mulFourierSeries (fourierCoeff f) ∘SL mulFourierSeries (fourierCoeff g) = mulFourierSeries (fourierCoeff fun (x : AddCircle T) => f x * g x)

Multiplication by the smooth function g followed by multiplication by the smooth function f is multiplication by f * g, on H^s for every real s.

@[simp]

theorem TauCeti.CircleSobolev.mulFourierSeries_fourierCoeff_one {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {T : ℝ} [Fact (0 < T)] : mulFourierSeries (fourierCoeff fun (x : AddCircle T) => 1) = ContinuousLinearMap.id ℂ (CircleSobolev s E)

Multiplication by the constant function 1 is the identity.

noncomputable def TauCeti.CircleSobolev.mulFourierSeriesEquiv {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {T : ℝ} [Fact (0 < T)] (f : AddCircle T → ℂ) (hf : ContDiff ℝ ↑⊤ fun (x : ℝ) => f ↑x) (hf₀ : ∀ (x : AddCircle T), f x ≠ 0) : CircleSobolev s E ≃L[ℂ] CircleSobolev s E

For a smooth function f on the circle that vanishes nowhere, multiplication by f as a continuous linear automorphism of H^s, for every real s; its inverse is multiplication by f⁻¹.

@[simp]

theorem TauCeti.CircleSobolev.coe_mulFourierSeriesEquiv {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {T : ℝ} [Fact (0 < T)] (f : AddCircle T → ℂ) (hf : ContDiff ℝ ↑⊤ fun (x : ℝ) => f ↑x) (hf₀ : ∀ (x : AddCircle T), f x ≠ 0) : ⇑(mulFourierSeriesEquiv f hf hf₀) = ⇑(mulFourierSeries (fourierCoeff f))

@[simp]

theorem TauCeti.CircleSobolev.coe_mulFourierSeriesEquiv_symm {s : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {T : ℝ} [Fact (0 < T)] (f : AddCircle T → ℂ) (hf : ContDiff ℝ ↑⊤ fun (x : ℝ) => f ↑x) (hf₀ : ∀ (x : AddCircle T), f x ≠ 0) : ⇑(mulFourierSeriesEquiv f hf hf₀).symm = ⇑(mulFourierSeries (fourierCoeff fun (x : AddCircle T) => (f x)⁻¹))

Multiplication by essentially bounded functions on H⁰

noncomputable def TauCeti.CircleSobolev.multiplicationOperator {T : ℝ} [Fact (0 < T)] (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : CircleSobolev 0 ℂ →L[ℂ] CircleSobolev 0 ℂ

Multiplication by an essentially bounded function a on H⁰ = L²: the multiplication operator MeasureTheory.Lp.multiplicationOperator a, transported along CircleSobolev.toLpₗᵢ.

@[simp]

theorem TauCeti.CircleSobolev.toLpₗᵢ_multiplicationOperator {T : ℝ} [Fact (0 < T)] (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (u : CircleSobolev 0 ℂ) : (toLpₗᵢ T) ((multiplicationOperator a) u) = (MeasureTheory.Lp.multiplicationOperator a) ((toLpₗᵢ T) u)

The L² function of a · u is the L² multiplication operator of a applied to that of u.

theorem TauCeti.CircleSobolev.toLpₗᵢ_multiplicationOperator_ae {T : ℝ} [Fact (0 < T)] (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (u : CircleSobolev 0 ℂ) : ↑↑((toLpₗᵢ T) ((multiplicationOperator a) u)) =ᵐ[AddCircle.haarAddCircle] fun (x : AddCircle T) => ↑↑a x * ↑↑((toLpₗᵢ T) u) x

Multiplication by a on H⁰ is pointwise multiplication almost everywhere.

theorem TauCeti.CircleSobolev.norm_multiplicationOperator_apply_le {T : ℝ} [Fact (0 < T)] (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (u : CircleSobolev 0 ℂ) : ‖(multiplicationOperator a) u‖ ≤ ‖a‖ * ‖u‖

Multiplication by a changes the H⁰ norm by at most ‖a‖∞.

@[simp]

theorem TauCeti.CircleSobolev.multiplicationOperator_zero {T : ℝ} [Fact (0 < T)] : multiplicationOperator 0 = 0

Multiplication by the zero symbol is the zero operator on H⁰.

@[simp]

theorem TauCeti.CircleSobolev.multiplicationOperator_add {T : ℝ} [Fact (0 < T)] (a b : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : multiplicationOperator (a + b) = multiplicationOperator a + multiplicationOperator b

Multiplication operators on H⁰ depend additively on their symbols.

@[simp]

theorem TauCeti.CircleSobolev.multiplicationOperator_smul {T : ℝ} [Fact (0 < T)] (c : ℂ) (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : multiplicationOperator (c • a) = c • multiplicationOperator a

Multiplication operators on H⁰ depend complex-linearly on their symbols.

theorem TauCeti.CircleSobolev.multiplicationOperator_comp_multiplicationOperator {T : ℝ} [Fact (0 < T)] (a b : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : multiplicationOperator a ∘SL multiplicationOperator b = multiplicationOperator (a * b)

Composing multiplication operators on H⁰ multiplies their symbols in the same order.

theorem TauCeti.CircleSobolev.mulFourierSeries_fourierCoeff_eq_multiplicationOperator {T : ℝ} [Fact (0 < T)] {f : C(AddCircle T, ℂ)} (hf : ContDiff ℝ ↑⊤ fun (x : ℝ) => f ↑x) : mulFourierSeries (fourierCoeff ⇑f) = multiplicationOperator ((ContinuousMap.toLp ⊤ AddCircle.haarAddCircle ℂ) f)

On H⁰ = L², multiplication by a smooth function f through its Fourier coefficients is the multiplication operator by f.