Products on the circle Sobolev spaces H^s for s > 1/2

For s > 1/2 the Fourier-coefficient Sobolev space H^s of the circle is an algebra: the product of two functions corresponds to the convolution of their Fourier coefficients, and convolution maps H^s × H^s boundedly to H^s. More generally, a continuous bilinear map L : E →L[ℂ] E' →L[ℂ] F induces a bounded bilinear map H^s(E) × H^s(E') → H^s(F), which on continuous representatives is x ↦ L (a x) (b x).

The coefficient estimate is DiscreteConvolution.tsum_sq_one_add_abs_rpow_mul_norm_addConvolution_le; this file transfers it to the spaces TauCeti.CircleSobolev s E and identifies the result with pointwise products of the continuous functions CircleSobolev.toContinuousMap.

Main definitions

• TauCeti.CircleSobolev.convolution hs L: for s > 1/2, the continuous bilinear map H^s(E) → H^s(E') → H^s(F) whose coefficients are the discrete convolution a.coeff ⋆₊[L] b.coeff.
• For a complete normed ℂ-algebra A and [Fact (1 / 2 < s)], the ring structure on CircleSobolev s A with this product and unit single 0 1 (commutative when A is), and the algebra structure over ℂ.
• TauCeti.CircleSobolev.toContinuousMapAlgHom: toContinuousMap as an algebra homomorphism H^s(A) →ₐ[ℂ] C(AddCircle T, A).

Main statements

• TauCeti.CircleSobolev.norm_convolution_le: the product estimate ‖convolution hs L a b‖ ≤ 2 ^ (s + 1) √(∑ₙ (1 + |n|) ^ (-2 s)) ‖L‖ ‖a‖ ‖b‖.
• TauCeti.CircleSobolev.toContinuousMap_convolution_apply: on continuous representatives the bilinear map is pointwise, x ↦ L (a x) (b x).
• TauCeti.CircleSobolev.toContinuousMap_mul and TauCeti.CircleSobolev.norm_mul_le: the product of H^s(A) is the pointwise product, and ‖a * b‖ ≤ 2 ^ (s + 1) √(∑ₙ (1 + |n|) ^ (-2 s)) ‖a‖ ‖b‖.
• TauCeti.CircleSobolev.norm_list_prod_le and TauCeti.CircleSobolev.norm_pow_le: the same estimate for finite products and powers, ‖a ^ k‖ ≤ mulConst s ^ (k - 1) ‖a‖ ^ k, where TauCeti.CircleSobolev.mulConst s is the maximum of 1 and the constant above.

References

• M. E. Taylor, Partial Differential Equations III, Chapter 13, Section 3 (Sobolev spaces as algebras).
• J. W. Robbin and D. A. Salamon, A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 8 (2006), 611–699 (products of boundary maps in Hardy decompositions).

The bilinear product

noncomputable def TauCeti.CircleSobolev.convolution {s : ℝ} {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup E'] [NormedSpace ℂ E'] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (hs : 1 / 2 < s) (L : E →L[ℂ] E' →L[ℂ] F) : CircleSobolev s E →L[ℂ] CircleSobolev s E' →L[ℂ] CircleSobolev s F

The product on H^s, s > 1/2. A continuous bilinear map L : E →L[ℂ] E' →L[ℂ] F induces the continuous bilinear map H^s(E) → H^s(E') → H^s(F) sending a and b to the element with coefficients a.coeff ⋆₊[L] b.coeff, the discrete convolution of their coefficients. On continuous representatives it is the pointwise map x ↦ L (a x) (b x) (CircleSobolev.toContinuousMap_convolution_apply).

@[simp]

theorem TauCeti.CircleSobolev.coeff_convolution {s : ℝ} {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup E'] [NormedSpace ℂ E'] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (hs : 1 / 2 < s) (L : E →L[ℂ] E' →L[ℂ] F) (a : CircleSobolev s E) (b : CircleSobolev s E') : (((convolution hs L) a) b).coeff = DiscreteConvolution.addConvolution (ContinuousLinearMap.toLinearMap₁₂ L) a.coeff b.coeff

theorem TauCeti.CircleSobolev.coeff_convolution_apply {s : ℝ} {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup E'] [NormedSpace ℂ E'] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (hs : 1 / 2 < s) (L : E →L[ℂ] E' →L[ℂ] F) (a : CircleSobolev s E) (b : CircleSobolev s E') (n : ℤ) : (((convolution hs L) a) b).coeff n = ∑' (m : ℤ), (L (a.coeff (n - m))) (b.coeff m)

The coefficients of the product are the convolution sums ∑ₘ L (a.coeff (n - m)) (b.coeff m).

theorem TauCeti.CircleSobolev.hasSum_coeff_convolution {s : ℝ} {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup E'] [NormedSpace ℂ E'] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (hs : 1 / 2 < s) (L : E →L[ℂ] E' →L[ℂ] F) (a : CircleSobolev s E) (b : CircleSobolev s E') (n : ℤ) : HasSum (fun (m : ℤ) => (L (a.coeff (n - m))) (b.coeff m)) ((((convolution hs L) a) b).coeff n)

The convolution sums defining the coefficients of the product converge.

theorem TauCeti.CircleSobolev.norm_convolution_le {s : ℝ} {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup E'] [NormedSpace ℂ E'] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (hs : 1 / 2 < s) (L : E →L[ℂ] E' →L[ℂ] F) (a : CircleSobolev s E) (b : CircleSobolev s E') : ‖((convolution hs L) a) b‖ ≤ 2 ^ (s + 1) * √(∑' (n : ℤ), weight (-(2 * s)) n) * ‖L‖ * ‖a‖ * ‖b‖

The product estimate on H^s, s > 1/2: ‖convolution hs L a b‖ ≤ 2 ^ (s + 1) √(∑ₙ (1 + |n|) ^ (-2 s)) ‖L‖ ‖a‖ ‖b‖.

theorem TauCeti.CircleSobolev.opNorm_convolution_le {s : ℝ} {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup E'] [NormedSpace ℂ E'] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (hs : 1 / 2 < s) (L : E →L[ℂ] E' →L[ℂ] F) : ‖convolution hs L‖ ≤ 2 ^ (s + 1) * √(∑' (n : ℤ), weight (-(2 * s)) n) * ‖L‖

@[simp]

theorem TauCeti.CircleSobolev.convolution_single_single {s : ℝ} {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup E'] [NormedSpace ℂ E'] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (hs : 1 / 2 < s) (L : E →L[ℂ] E' →L[ℂ] F) (m n : ℤ) (x : E) (y : E') : ((convolution hs L) ((single m) x)) ((single n) y) = (single (m + n)) ((L x) y)

@[simp]

theorem TauCeti.CircleSobolev.convolution_inclusion {s : ℝ} {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup E'] [NormedSpace ℂ E'] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {t : ℝ} (ht : 1 / 2 < t) (h : t ≤ s) (L : E →L[ℂ] E' →L[ℂ] F) (a : CircleSobolev s E) (b : CircleSobolev s E') : ((convolution ht L) ((inclusion h) a)) ((inclusion h) b) = (inclusion h) (((convolution ⋯ L) a) b)

The bilinear map convolution hs L commutes with the inclusions H^s → H^t, 1/2 < t ≤ s.

@[simp]

theorem TauCeti.CircleSobolev.toContinuousMap_convolution_apply {s : ℝ} {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup E'] [NormedSpace ℂ E'] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (T : ℝ) [Fact (0 < T)] [CompleteSpace E] [CompleteSpace E'] (hs : 1 / 2 < s) (L : E →L[ℂ] E' →L[ℂ] F) (a : CircleSobolev s E) (b : CircleSobolev s E') (x : AddCircle T) : ((toContinuousMap T hs) (((convolution hs L) a) b)) x = (L (((toContinuousMap T hs) a) x)) (((toContinuousMap T hs) b) x)

On continuous representatives the product is pointwise: for s > 1/2, the continuous function attached to convolution hs L a b is x ↦ L (a x) (b x).

The algebra H^s(A)

noncomputable def TauCeti.CircleSobolev.mulConst (s : ℝ) : ℝ

The constant of the product estimate for finite products in H^s: the maximum of 1 and the constant 2 ^ (s + 1) √(∑ₙ (1 + |n|) ^ (-2 s)) of norm_mul_le.

theorem TauCeti.CircleSobolev.one_le_mulConst {s : ℝ} : 1 ≤ mulConst s

@[instance_reducible]

noncomputable instance TauCeti.CircleSobolev.instOne {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] : One (CircleSobolev s A)

The unit of H^s(A): the constant function 1.

theorem TauCeti.CircleSobolev.one_def {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] : 1 = (single 0) 1

@[simp]

theorem TauCeti.CircleSobolev.coeff_one {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] : coeff 1 = Pi.single 0 1

@[instance_reducible]

noncomputable instance TauCeti.CircleSobolev.instMul {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] : Mul (CircleSobolev s A)

For s > 1/2, the product on H^s(A): the convolution of the coefficients.

theorem TauCeti.CircleSobolev.mul_def {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (a b : CircleSobolev s A) : a * b = ((convolution ⋯ (ContinuousLinearMap.mul ℂ A)) a) b

@[simp]

theorem TauCeti.CircleSobolev.coeff_mul {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (a b : CircleSobolev s A) (n : ℤ) : (a * b).coeff n = ∑' (m : ℤ), a.coeff (n - m) * b.coeff m

The coefficients of a product are the convolution sums ∑ₘ a.coeff (n - m) * b.coeff m.

theorem TauCeti.CircleSobolev.hasSum_coeff_mul {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (a b : CircleSobolev s A) (n : ℤ) : HasSum (fun (m : ℤ) => a.coeff (n - m) * b.coeff m) ((a * b).coeff n)

@[simp]

theorem TauCeti.CircleSobolev.single_mul_single {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (m n : ℤ) (x y : A) : (single m) x * (single n) y = (single (m + n)) (x * y)

theorem TauCeti.CircleSobolev.norm_mul_le {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (a b : CircleSobolev s A) : ‖a * b‖ ≤ 2 ^ (s + 1) * √(∑' (n : ℤ), weight (-(2 * s)) n) * ‖a‖ * ‖b‖

The product estimate in H^s(A), s > 1/2.

@[simp]

theorem TauCeti.CircleSobolev.toContinuousMap_mul {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] (a b : CircleSobolev s A) : (toContinuousMap T ⋯) (a * b) = (toContinuousMap T ⋯) a * (toContinuousMap T ⋯) b

On continuous representatives the product of H^s(A) is the pointwise product.

@[simp]

theorem TauCeti.CircleSobolev.toContinuousMap_one {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] : (toContinuousMap T ⋯) 1 = 1

@[instance_reducible]

noncomputable instance TauCeti.CircleSobolev.instRing {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] : Ring (CircleSobolev s A)

For s > 1/2, H^s(A) is a ring under the convolution product, with unit single 0 1.

@[instance_reducible]

noncomputable instance TauCeti.CircleSobolev.instAlgebraComplex {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] : Algebra ℂ (CircleSobolev s A)

For s > 1/2, H^s(A) is a ℂ-algebra.

theorem TauCeti.CircleSobolev.algebraMap_eq_single {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (c : ℂ) : (algebraMap ℂ (CircleSobolev s A)) c = (single 0) ((algebraMap ℂ A) c)

instance TauCeti.CircleSobolev.instIsTopologicalRing {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] : IsTopologicalRing (CircleSobolev s A)

The product of H^s(A) is continuous, since it is a bounded bilinear map.

theorem TauCeti.CircleSobolev.norm_mul_le_mulConst {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (a b : CircleSobolev s A) : ‖a * b‖ ≤ mulConst s * ‖a‖ * ‖b‖

The product estimate norm_mul_le, with the constant mulConst s.

theorem TauCeti.CircleSobolev.norm_list_prod_le {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] [NormOneClass A] (l : List (CircleSobolev s A)) : ‖l.prod‖ ≤ mulConst s ^ (l.length - 1) * (List.map norm l).prod

The product estimate for a finite product in H^s(A): ‖a₁ ⋯ aₖ‖ ≤ mulConst s ^ (k - 1) ‖a₁‖ ⋯ ‖aₖ‖, with natural-number subtraction.

theorem TauCeti.CircleSobolev.norm_pow_le {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] [NormOneClass A] (a : CircleSobolev s A) (k : ℕ) : ‖a ^ k‖ ≤ mulConst s ^ (k - 1) * ‖a‖ ^ k

The product estimate for powers in H^s(A): ‖a ^ k‖ ≤ mulConst s ^ (k - 1) ‖a‖ ^ k, with natural-number subtraction.

noncomputable def TauCeti.CircleSobolev.toContinuousMapAlgHom {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] : CircleSobolev s A →ₐ[ℂ] C(AddCircle T, A)

For s > 1/2, toContinuousMap is an algebra homomorphism H^s(A) → C(AddCircle T, A).

@[simp]

theorem TauCeti.CircleSobolev.coe_toContinuousMapAlgHom {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] : ⇑(toContinuousMapAlgHom T) = ⇑(toContinuousMap T ⋯)

@[simp]

theorem TauCeti.CircleSobolev.toContinuousMap_pow {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] (a : CircleSobolev s A) (k : ℕ) : (toContinuousMap T ⋯) (a ^ k) = (toContinuousMap T ⋯) a ^ k

On continuous representatives the powers of H^s(A) are the pointwise powers.

@[instance_reducible]

noncomputable instance TauCeti.CircleSobolev.instCommRing {s : ℝ} {A : Type u_4} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] : CommRing (CircleSobolev s A)

For s > 1/2 and a commutative A, H^s(A) is a commutative ring.