Bourbaki's locally convex extension of Banach–Alaoglu

banach_alaoglu_bourbaki

Submitter: Kim Morrison.

Notes: §137 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. Bourbaki's locally convex Banach–Alaoglu theorem states that, for any real locally convex topological vector space E, the weak-star polar of a neighbourhood of 0 is compact in the weak dual. This extends the familiar normed-space Banach–Alaoglu theorem from closed dual balls to polars of zero-neighbourhoods in arbitrary locally convex spaces. Mathlib currently has the normed-space results WeakDual.isCompact_closedBall and WeakDual.isCompact_polar, but no corresponding compactness theorem for general locally convex spaces.

Source: N. Bourbaki, Espaces vectoriels topologiques; the normed case is L. Alaoglu, Ann. of Math. 41 (1940). Listed as §137 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Realise each functional φ ∈ WeakDual ℝ E by its restriction to the neighbourhood U, embedding the polar into the product ∏_{x ∈ U} [−1, 1] (φ ↦ (φ x)). The polar maps into this product because |φ x| ≤ 1 on U; by Tychonoff the product is compact. The image is closed: the conditions ‖φ x‖ ≤ 1 (closed) and linearity/continuity of φ (preserved under pointwise limits, using that U absorbs E so a pointwise limit of equicontinuous functionals is again continuous and linear) are closed in the product topology, which coincides with the weak-star topology on the polar. Hence the polar is a closed subset of a compact space, so compact.

theorem declaration uses `sorry`banach_alaoglu_bourbaki (E : Type*) [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E]
    [LocallyConvexSpace ℝ E] (U : Set E) (_hU : U ∈ 𝓝 (0 : E)) :
    IsCompact (LeanEval.Analysis.weakStarPolar E U) := byE:Type u_1inst✝⁵:AddCommGroup Einst✝⁴:Module ℝ Einst✝³:TopologicalSpace Einst✝²:ContinuousAdd Einst✝¹:ContinuousSMul ℝ Einst✝:LocallyConvexSpace ℝ EU:Set E_hU:U ∈ 𝓝 0⊢ IsCompact (weakStarPolar E U)
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 1, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 2, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on Jun 3, 2026

• @rishistyping with Stealth Model on Jun 7, 2026