Weak compactness of Hilbert closed balls

If E is a (real or complex) Hilbert space, then the norm-closed ball is compact in the weak topology on E.

This is a “Riesz + Banach–Alaoglu” bridge:

• Use the Riesz representation theorem (InnerProductSpace.toDual) to identify E with its continuous dual.
• Transfer Banach–Alaoglu compactness (WeakDual.isCompact_closedBall) to WeakSpace 𝕜 E.

This lemma is a key building block for developing compact/self-adjoint spectral theory in a Hilbert setting while keeping packages/mathlib_extensions/ mathlib-only.

@[implicit_reducible]

noncomputable def CompactSpectral.instNormWeakSpace {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Norm (WeakSpace 𝕜 E)

Norm on WeakSpace 𝕜 E inherited from E. Since WeakSpace 𝕜 E := E, this lets us write ‖x‖ for x : WeakSpace 𝕜 E without explicit coercion.

Equations

• CompactSpectral.instNormWeakSpace = { norm := norm }

Weak ↔ weak-star maps via Riesz

noncomputable def CompactSpectral.weakToWeakDual {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : WeakSpace 𝕜 E → WeakDual 𝕜 E

The Riesz map E → E* viewed as a function from the weak topology on E (WeakSpace 𝕜 E) to the weak-star topology on the dual (WeakDual 𝕜 E).

Equations

• CompactSpectral.weakToWeakDual x = StrongDual.toWeakDual ((InnerProductSpace.toDual 𝕜 E) x)

noncomputable def CompactSpectral.weakDualToWeak {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : WeakDual 𝕜 E → WeakSpace 𝕜 E

The inverse Riesz map E* → E viewed as a function from the weak-star dual (WeakDual 𝕜 E) to the weak topology on E (WeakSpace 𝕜 E).

Equations

• CompactSpectral.weakDualToWeak f = (InnerProductSpace.toDual 𝕜 E).symm (WeakDual.toStrongDual f)

theorem CompactSpectral.continuous_weakToWeakDual {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : Continuous weakToWeakDual

theorem CompactSpectral.continuous_weakDualToWeak {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : Continuous weakDualToWeak

Closed balls

noncomputable def CompactSpectral.weakClosedBall {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (r : ℝ) : Set (WeakSpace 𝕜 E)

The norm-closed ball, viewed as a subset of WeakSpace 𝕜 E.

Equations

• CompactSpectral.weakClosedBall r = Metric.closedBall 0 r

noncomputable def CompactSpectral.weakDualClosedBall {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (r : ℝ) : Set (WeakDual 𝕜 E)

The (weak-*) closed ball in the dual, as a subset of WeakDual 𝕜 E.

Equations

• CompactSpectral.weakDualClosedBall r = (fun (f : WeakDual 𝕜 E) => WeakDual.toStrongDual f) ⁻¹' Metric.closedBall 0 r

theorem CompactSpectral.isCompact_weakClosedBall {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (r : ℝ) : IsCompact (weakClosedBall r)

In a Hilbert space E, the norm-closed ball is compact for the weak topology.