Approximate identities on a compact group

Convolution against a continuous kernel smooths an L² class into a continuous function (TauCeti.convolutionCLM). This file supplies the kernels that make that smoothing harmless: for every neighbourhood U of the identity there is a mollifying kernel supported in U, and convolving a continuous function against a kernel supported in a small enough neighbourhood changes it by as little as one likes in the uniform norm.

A mollifying kernel is bundled as TauCeti.IsMollifier U k: the kernel is nonnegative, invariant under inversion, has unit mass for normalized Haar measure, and vanishes off U. Inversion invariance of a nonnegative kernel is the symmetry k g⁻¹ = conj (k g), so convolutionOperator k is self-adjoint (TauCeti.IsMollifier.isSelfAdjoint_convolutionOperator); this is one of the two hypotheses of the spectral theorem for compact self-adjoint operators, the other, compactness, being no concern of this file.

Main definitions

• TauCeti.IsMollifier: k is a nonnegative, inversion-invariant, unit-mass continuous kernel vanishing outside U.

Main statements

• TauCeti.exists_mem_nhds_one_norm_sub_le: uniform continuity of a continuous function on a compact group, in the form ‖f (z⁻¹ * x) - f x‖ ≤ ε for z near 1, uniformly in x.
• TauCeti.exists_isMollifier: mollifying kernels exist supported in any neighbourhood of 1.
• TauCeti.IsMollifier.norm_convolutionCLM_toLp_sub_le: the uniform estimate ‖k * f - f‖ ≤ ε for a kernel supported where f varies by at most ε.
• TauCeti.exists_isMollifier_norm_convolutionCLM_toLp_sub_le: the approximate identity. For every continuous f, every ε > 0 and every neighbourhood U of 1 there is a mollifying kernel supported in U with ‖k * f - f‖ ≤ ε.
• TauCeti.tendsto_convolutionCLM_toLp: the same statement as convergence of a net of kernels whose supports shrink to 1.
• TauCeti.exists_isMollifier_tendsto_convolutionCLM_toLp: the approximate identity as a single family. One mollifying kernel for each neighbourhood of 1, whose convolutions converge uniformly to f as the neighbourhood shrinks, simultaneously for every continuous f.

Implementation notes

Uniform continuity is obtained from the same currying trick that builds the kernel sections in TauCeti/RepresentationTheory/Compact/Convolution.lean: the left translates z ↦ (x ↦ f (z⁻¹ * x)) assemble into a continuous map G → C(G, 𝕜) for the uniform norm, and continuity at z = 1 is exactly the uniform estimate. No uniform structure on G is mentioned.

The kernels themselves come from Urysohn's lemma, in the form that asks for a regular, locally compact space: a compact topological group is both whether or not it is Hausdorff, so the construction needs no T2Space G, and the mollifier results below do not assume it. A bump at the identity supported in a symmetric neighbourhood is made inversion invariant by adding its composition with inversion, and then normalized by its mass, which is positive because Haar measure is positive on nonempty open sets.

Kernels take values in 𝕜 rather than in ℝ because that is what convolutionCLM consumes; nonnegativity is stated with the scoped ComplexOrder instance on an RCLike field, for which 0 ≤ z means z is real and nonnegative.

References

This is approx_identity_exists from Layer 5 of the compact-groups roadmap, the last input to the uniform density of the matrix coefficients in C(G) that the roadmap's non-circular route to the Peter-Weyl theorem requires.

• G. B. Folland, A Course in Abstract Harmonic Analysis, 2nd ed., CRC (2016), Chapter 5.
• D. Bump, Lie Groups, 2nd ed., Springer GTM 225 (2013), Chapter 2.

Uniform continuity on a compact group

theorem TauCeti.exists_mem_nhds_one_norm_sub_le {E : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (f : C(G, E)) {ε : ℝ} (hε : 0 < ε) : ∃ V ∈ nhds 1, ∀ z ∈ V, ∀ (x : G), ‖f (z⁻¹ * x) - f x‖ ≤ ε

Uniform continuity of a continuous function on a compact group. For every ε > 0 there is a neighbourhood V of the identity such that translating the argument by any z ∈ V moves the value of f by at most ε, uniformly in the argument.

The uniform structure of G is not mentioned: the statement is continuity at z = 1 of the map sending z to the left translate of f by z, which is continuous into C(G, E) for the uniform norm because G is compact.

Mollifying kernels

structure TauCeti.IsMollifier {𝕜 : Type u_1} {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (U : Set G) (k : C(G, 𝕜)) : Prop

A mollifying kernel supported in U: a continuous kernel on a compact group which is nonnegative, invariant under inversion, of unit mass for normalized Haar measure, and zero outside U.

Nonnegativity is taken in the scoped ComplexOrder order of the RCLike field 𝕜, so it says in particular that k is real-valued. Together with inversion invariance it gives the symmetry k g⁻¹ = conj (k g) that makes convolutionOperator k self-adjoint.

• nonneg (g : G) : 0 ≤ k g

  A mollifying kernel is nonnegative, hence real-valued.

• inv_apply (g : G) : k g⁻¹ = k g

  A mollifying kernel is invariant under inversion.

• integral_eq_one : ∫ (g : G), k g ∂haarProb G = 1

  A mollifying kernel has unit mass for normalized Haar measure.

• eq_zero_of_notMem (g : G) : g ∉ U → k g = 0

  A mollifying kernel supported in U vanishes outside U.

theorem TauCeti.IsMollifier.mono {𝕜 : Type u_1} {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {U U' : Set G} {k : C(G, 𝕜)} (h : IsMollifier U k) (hUU' : U ⊆ U') : IsMollifier U' k

Enlarging the neighbourhood a kernel is supported in.

theorem TauCeti.IsMollifier.apply_eq_norm {𝕜 : Type u_1} {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {U : Set G} {k : C(G, 𝕜)} (h : IsMollifier U k) (g : G) : k g = ↑‖k g‖

A mollifying kernel is its own norm: it takes nonnegative real values.

theorem TauCeti.IsMollifier.inv_apply_eq_conj {𝕜 : Type u_1} {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {U : Set G} {k : C(G, 𝕜)} (h : IsMollifier U k) (g : G) : k g⁻¹ = (starRingEnd 𝕜) (k g)

A mollifying kernel is symmetric in the sense required for self-adjointness of the associated convolution operator: inversion invariance and real-valuedness combine to k g⁻¹ = conj (k g).

theorem TauCeti.IsMollifier.isSelfAdjoint_convolutionOperator {𝕜 : Type u_1} {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {U : Set G} {k : C(G, 𝕜)} (h : IsMollifier U k) : IsSelfAdjoint (convolutionOperator k)

The convolution operator of a mollifying kernel is self-adjoint. This is one of the two hypotheses of the spectral theorem for compact self-adjoint operators; compactness of convolutionOperator k is a separate matter, not established here.

theorem TauCeti.IsMollifier.integral_norm_eq_one {𝕜 : Type u_1} {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {U : Set G} {k : C(G, 𝕜)} (h : IsMollifier U k) : ∫ (g : G), ‖k g‖ ∂haarProb G = 1

A mollifying kernel has unit L¹ norm.

theorem TauCeti.exists_isMollifier (𝕜 : Type u_1) {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {U : Set G} (hU : U ∈ nhds 1) : ∃ (k : C(G, 𝕜)), IsMollifier U k

Mollifying kernels exist, supported in any prescribed neighbourhood of the identity.

The kernel is built from a Urysohn bump at the identity supported in a symmetric open neighbourhood, made inversion invariant by adding its composition with inversion, and normalized by its mass, which is positive because Haar measure is positive on nonempty open sets.

Approximate-identity estimates

theorem TauCeti.IsMollifier.norm_convolutionCLM_toLp_sub_le {𝕜 : Type u_1} {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {U : Set G} {k : C(G, 𝕜)} (h : IsMollifier U k) (f : C(G, 𝕜)) {ε : ℝ} (hε : 0 ≤ ε) (hf : ∀ z ∈ U, ∀ (x : G), ‖f (z⁻¹ * x) - f x‖ ≤ ε) : ‖(convolutionCLM k) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) f) - f‖ ≤ ε

The approximate-identity estimate. If a mollifying kernel is supported where f varies by at most ε, then convolving f against it changes f by at most ε in the uniform norm.

theorem TauCeti.exists_isMollifier_norm_convolutionCLM_toLp_sub_le (𝕜 : Type u_1) {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (f : C(G, 𝕜)) {ε : ℝ} (hε : 0 < ε) {U : Set G} (hU : U ∈ nhds 1) : ∃ (k : C(G, 𝕜)), IsMollifier U k ∧ ‖(convolutionCLM k) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) f) - f‖ ≤ ε

Approximate identities exist on a compact group. For every continuous f, every ε > 0 and every neighbourhood U of the identity there is a mollifying kernel supported in U whose convolution with f is uniformly within ε of f.

This is the input to the uniform density of the matrix coefficients in C(G): a continuous function is approximated by convolutions, and convolutions are decomposed spectrally into finitely many matrix coefficients.

theorem TauCeti.exists_isMollifier_convolutionOperator_toLp_ne_zero (𝕜 : Type u_1) {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {f : C(G, 𝕜)} (hf : f ≠ 0) {U : Set G} (hU : U ∈ nhds 1) : ∃ (k : C(G, 𝕜)), IsMollifier U k ∧ (convolutionOperator k) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) f) ≠ 0

The mollifying convolution operators are jointly nondegenerate. No nonzero continuous function is annihilated by every mollifying convolution operator, because convolving against a kernel supported near the identity moves a function by less than its own norm.

This is why the Peter-Weyl argument can start: together with the self-adjointness above, and with compactness of convolutionOperator k established elsewhere, it supplies a nonzero operator to feed to the spectral theorem. Nonvanishing and self-adjointness are what is proved here; compactness is not.

theorem TauCeti.tendsto_convolutionCLM_toLp {𝕜 : Type u_1} {G : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {ι : Type u_4} {l : Filter ι} {U : ι → Set G} {k : ι → C(G, 𝕜)} (hk : ∀ᶠ (i : ι) in l, IsMollifier (U i) (k i)) (hU : ∀ V ∈ nhds 1, ∀ᶠ (i : ι) in l, U i ⊆ V) (f : C(G, 𝕜)) : Filter.Tendsto (fun (i : ι) => (convolutionCLM (k i)) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) f)) l (nhds f)

The approximate identity as a net. If the kernels k i are eventually mollifying kernels whose supporting neighbourhoods U i eventually shrink inside every neighbourhood of the identity, then k i * f converges uniformly to f for every continuous f.

theorem TauCeti.exists_isMollifier_tendsto_convolutionCLM_toLp (𝕜 : Type u_1) (G : Type u_3) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : ∃ (k : { U : Set G // U ∈ nhds 1 } → C(G, 𝕜)), (∀ (U : { U : Set G // U ∈ nhds 1 }), IsMollifier (↑U) (k U)) ∧ ∀ (f : C(G, 𝕜)), Filter.Tendsto (fun (U : { U : Set G // U ∈ nhds 1 }) => (convolutionCLM (k U)) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) f)) (Filter.comap Subtype.val (nhds 1).smallSets) (nhds f)

The approximate identity itself: a single family of mollifying kernels that works for every function. There is a kernel k U for each neighbourhood U of the identity, mollifying and supported in U, such that for every continuous f the convolutions k U * f converge uniformly to f as U shrinks to the identity.

The index filter is the one of TauCeti.comap_val_smallSets_neBot at 𝓝 1, which is nontrivial, so the convergence has content. Unlike TauCeti.exists_isMollifier_norm_convolutionCLM_toLp_sub_le, where the kernel may depend on the function being approximated, the family here is chosen once and for all.