feat(Analysis/LocallyConvex/Polar): Bipolar theorem by mans0954 · Pull Request #26345 · leanprover-community/mathlib4

mans0954 · 2025-06-24T07:30:24Z

The bipolar theorem states that the polar of the polar of a set s is equal to the closed absolutely convex hull of s.

The argument here follows Conway, Chapter V. 1.8.

This PR continues the work from #20843.

Original PR: #20843

depends on: [Merged by Bors] - feat(Analysis/LocallyConvex/WeakDual): characterise the span of some functionals with continuity #27316

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

This reverts commit f8148c2.

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

@mans0954

…35422) This PR uses the material in Topology/Algebra/Module/WeakBilin.lean from the unfinished PR #26345 by @mans0954. Given a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`, every continuous functional on `E` endowed with the `σ(E, F; B)`-topology is of the form `x ↦ B(x, y)` for some `y : F`. The result doesn't generally seem to be named, but Narici-Beckenstein's "Topological Vector Spaces" calls it the "weak representation theorem", a term we have used for the docstring. Co-authored-by: David Gross <david.gross@thp.uni-koeln.de>

@mans0954

…eanprover-community#35422) This PR uses the material in Topology/Algebra/Module/WeakBilin.lean from the unfinished PR leanprover-community#26345 by @mans0954. Given a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`, every continuous functional on `E` endowed with the `σ(E, F; B)`-topology is of the form `x ↦ B(x, y)` for some `y : F`. The result doesn't generally seem to be named, but Narici-Beckenstein's "Topological Vector Spaces" calls it the "weak representation theorem", a term we have used for the docstring. Co-authored-by: David Gross <david.gross@thp.uni-koeln.de>

j-loreaux · 2026-03-23T16:14:21Z

I've discussed with Filippo, and due to time constraints for him, I will take over this PR.

mathlib-merge-conflicts · 2026-04-05T05:44:47Z

This pull request has conflicts, please merge master and resolve them.

themathqueen · 2026-04-05T12:34:06Z

  map_smul' _ _ := by ext; simp

+open LinearMap in
+lemma dualEmbedding_injective_of_separatingRight {E F : Type*} [AddCommGroup E] [AddCommGroup F]


shouldn't this be eval instead of dualEmbedding?

Suggested change

lemma dualEmbedding_injective_of_separatingRight {E F : Type*} [AddCommGroup E] [AddCommGroup F]

lemma eval_injective_of_separatingRight {E F : Type*} [AddCommGroup E] [AddCommGroup F]

Maybe.

The lemma got merged as #35422. We took the name from the existing PR. Should we change it? @j-loreaux?

I guess _root_.WeakBilin.eval_surjective would make sense.

faenuccio

I've left a bunch of comments, but beyond these it looks good to me.

faenuccio · 2026-04-19T11:40:41Z

    [AddCommMonoid F] [Module 𝕜 F] [SMul 𝕝 𝕜] [Module 𝕝 E] [s : IsScalarTower 𝕝 𝕜 E]
    (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : IsScalarTower 𝕝 𝕜 (WeakBilin B) := s

+/-- The canonical linear equivalence (over `𝕝`) between `WeakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)`


Suggested change

/-- The canonical linear equivalence (over `𝕝`) between `WeakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)`

/-- The linear equivalence (over `𝕝`) between `WeakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)`

faenuccio · 2026-04-19T11:47:35Z

+/-
+When `B` is left-separating, the closure of the empty set is the singleton `{0}`. This is in
+contrast to the closed absolutely convex hull of the empty set, which is again the empty set.
+c.f. `closureOperator_polar_gc_nonempty` below.


Suggested change

c.f. `closureOperator_polar_gc_nonempty` below.

cf. `closureOperator_polar_gc_nonempty` below.

faenuccio · 2026-04-19T11:48:44Z

+contrast to the closed absolutely convex hull of the empty set, which is again the empty set.
+c.f. `closureOperator_polar_gc_nonempty` below.
+-/
+example (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (h : SeparatingLeft B) :


Why is this an example?

faenuccio · 2026-04-19T11:51:20Z

+
+open WeakBilin
+/-
+The Bipolar Theorem: The bipolar of a set coincides with its closed absolutely convex hull.


I would add to this docstring some comment about the setting (what is 𝕜, what is E, what is B, etc) so that someone landing on the result can have a quick grasp of the situation.

faenuccio · 2026-04-19T11:54:19Z

+This fails when `s` is empty. Indeed, `closedAbsConvexHull (E := WeakBilin B) 𝕜 s` is the empty set,
+but `B.polar_gc.closureOperator s` equals `{0}` when `B` is left separating (see example above).
+-/


Suggested change

This fails when `s` is empty. Indeed, `closedAbsConvexHull (E := WeakBilin B) 𝕜 s` is the empty set,

but `B.polar_gc.closureOperator s` equals `{0}` when `B` is left separating (see example above).

-/

This fails when `s` is empty. Indeed, `closedAbsConvexHull (E := WeakBilin B) 𝕜 ∅` is the empty set,

but `B.polar_gc.closureOperator ∅` equals `{0}` when `B` is left separating (see example above).

-/

faenuccio · 2026-04-19T12:30:16Z

+    RCLike.geometric_hahn_banach_closed_point (𝕜 := 𝕜)
+      (by rw [← convex_RCLike_iff_convex_real (K := 𝕜)]; exact absConvex_convexClosedHull.2)
+      isClosed_closedAbsConvexHull hx
+  -- `0` is in `(closedAbsConvexHull 𝕜) s` so `u` must be strictly positive


Suggested change

-- `0` is in `(closedAbsConvexHull 𝕜) s` so `u` must be strictly positive

-- `0` is in `(closedAbsConvexHull 𝕜) s` so `u` must be strictly positive.

faenuccio · 2026-04-19T12:30:24Z

+  have f_zero_lt_u : RCLike.re (f 0) < u :=
+    (hf₁ 0) (absConvexHull_subset_closedAbsConvexHull zero_mem_absConvexHull)
+  rw [map_zero, map_zero] at f_zero_lt_u
+  -- Rescale `f` as `g` in order that for all `a` in `(closedAbsConvexHull 𝕜) s` `Re (g a) < 1`


Suggested change

-- Rescale `f` as `g` in order that for all `a` in `(closedAbsConvexHull 𝕜) s` `Re (g a) < 1`

-- Rescale `f` as `g` in order that for all `a` in `(closedAbsConvexHull 𝕜) s` `Re (g a) < 1`.

faenuccio · 2026-04-19T12:32:49Z

+    rw [fg, ContinuousLinearMap.coe_smul', Pi.smul_apply, RCLike.smul_re, one_div,
+      ← (inv_mul_cancel₀ (lt_iff_le_and_ne.mp f_zero_lt_u).2.symm)]
+    exact mul_lt_mul_of_pos_left ((hf₁ _) ha) (inv_pos_of_pos f_zero_lt_u)
+  -- The dual embedding is surjective, let `f₀` be the element of `F` corresponding to `g`


Suggested change

-- The dual embedding is surjective, let `f₀` be the element of `F` corresponding to `g`

-- The dual embedding is surjective, let `f₀` be the element of `F` corresponding to `g`:

faenuccio · 2026-04-19T12:33:57Z

+    exact mul_lt_mul_of_pos_left ((hf₁ _) ha) (inv_pos_of_pos f_zero_lt_u)
+  -- The dual embedding is surjective, let `f₀` be the element of `F` corresponding to `g`
+  obtain ⟨f₀, hf₀⟩ := (pairing B).dualEmbedding_surjective g
+  -- Then, by construction, `f₀` is in the polar of `s`


Suggested change

-- Then, by construction, `f₀` is in the polar of `s`

-- Then, by construction, `f₀` is in the polar of `s`.

faenuccio · 2026-04-19T12:53:48Z

+      ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_mk', Pi.smul_apply,
+      Algebra.mul_smul_comm]
+    rw [← smul_eq_mul, ← smul_assoc]
+    norm_cast
+    simp only [smul_eq_mul, mul_inv_cancel₀ (ne_of_lt f_zero_lt_u).symm, map_one, one_mul]
+    exact flip_apply ..


Suggested change

ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_mk', Pi.smul_apply,

Algebra.mul_smul_comm]

rw [← smul_eq_mul, ← smul_assoc]

norm_cast

simp only [smul_eq_mul, mul_inv_cancel₀ (ne_of_lt f_zero_lt_u).symm, map_one, one_mul]

exact flip_apply ..

simp only [← RCLike.re_ofReal_mul, map_inv₀, ← u_smul_g_eq_f, ← hf₀, WeakBilin.eval, coe_mk,

AddHom.coe_mk, ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_mk', Pi.smul_apply,

Algebra.mul_smul_comm]

rw [← smul_eq_mul, ← smul_assoc]

norm_cast

simp [mul_inv_cancel₀ (ne_of_lt f_zero_lt_u).symm, flip_apply]

j-loreaux · 2026-04-23T16:27:13Z

I have had some ideas about how to greatly improve the statement (as well as adding additional versions), but it requires a bigger refactor, so unfortunately this will sit a while longer, but it is on my TODO list with a relatively high priority.

I will address the comments above when I finish the background changes required.

…ject#17829) This PR proves the bipolar theorem for real and complex locally convex spaces. Characterize the closure of a nonempty absolutely convex set by the continuous linear functionals bounded by one on it, and identify the bipolar of any set with its closed absolutely convex hull after adjoining zero. Advance [BanachSpaceTheory/README.md, B1, “Duality and weak topologies”](https://github.com/TauCetiProject/TauCetiRoadmap/blob/main/BanachSpaceTheory/README.md#b1-duality-and-weak-topologies), specifically “Prove the bipolar theorem for absolutely convex sets.” This directly closes that named target using the merged polar and Hahn–Banach infrastructure. After this PR, outstanding B1 work includes Goldstine (TauCetiProject#17712), the norm double-annihilator theorem (TauCetiProject#16832), and the explicit compatible metric on separable dual balls. Open-work and recent-merge scans, focused bipolar searches, and searches of pinned Mathlib and Tau Ceti found no overlapping implementation. Cooperative claim registration returned the documented exit-2 fallback because canonical claim-ref writes were denied. Add `TauCeti/Analysis/LocallyConvex/Polar.lean` (66 lines) and `TauCeti/Analysis/LocallyConvex/Bipolar.lean` (111 lines): six theorems, with no new definitions, instances, or notation. The algebraic hull-invariance lemma works for any bilinear pairing of modules over an `RCLike` field, without topology or additive inverses. The bipolar theorems require neither completeness, separability, nor Hausdorffness. The arbitrary-set statement handles the empty set explicitly: Mathlib's absolutely convex hull of the empty set is empty, whereas a bipolar contains zero. Reuse `LinearMap.polar_AbsConvex`, the polar Galois connection, `RCLike.geometric_hahn_banach_closed_point`, and `RCLike.exists_norm_eq_mul_self`. The bipolar module cites Megginson, §2.6, and Christopher Hoskin's [Mathlib PR #26345](leanprover-community/mathlib4#26345), consulted for the bilinear-pairing formulation requested by the roadmap. No Mathlib infrastructure or external formalization is vendored. Read the shared protocol and all ten rubrics: scope, correctness, reuse, attribution, api-design, generality, placement, naming, documentation, and proof-quality. Self-review generalizes the algebraic hull lemma from the continuous dual to arbitrary bilinear pairings, weakens its additive assumptions to commutative monoids, and places it in the native `LinearMap` namespace in a separate polar module. The resulting API retains the separation witness, both bipolar forms, and a closed-hull membership criterion; the hull-invariance lemmas are registered for simplification. Repeated source searches found no existing replacement. Ordinary-import examples check a real open unit ball, a complex closed disk, the empty set, and a complex two-point hull. Foreground cache retrieval, the full library build, and the axiom audit pass. All 14 default environment linters report zero errors on the six new declarations. The whole-library style wrapper hits this host's command-line length limit; its unchanged header checker and Mathlib's text-style checker pass when run directly on the two new modules. Roadmap: BanachSpaceTheory  🤖 Prepared with Codex

mans0954 and others added 30 commits February 21, 2025 06:40

Merge branch 'master' into mans0954/polar_AbsConvex

740f01a

Merge branch 'master' into mans0954/bipolar-theorem

05996bf

Fix

497f32d

Fix

8c0e59c

Reduce imports

1e89144

Shake

22536f6

Merge branch 'master' into mans0954/polar_AbsConvex

0f66720

Order

89774b7

Merge branch 'master' into mans0954/polar_AbsConvex

d618236

Merge branch 'master' into mans0954/polar_AbsConvex

09e84fe

Merge branch 'master' into mans0954/polar_AbsConvex

4eb112f

Merge branch 'master' into mans0954/polar_AbsConvex

5d1a072

Update Mathlib/Analysis/LocallyConvex/Basic.lean

f8148c2

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Revert "Update Mathlib/Analysis/LocallyConvex/Basic.lean"

ef62918

This reverts commit f8148c2.

Update Mathlib/Analysis/Normed/Module/Dual.lean

93f8401

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Save the bipolar theorem to later

c7069a7

Merge branch 'master' into mans0954/polar_AbsConvex

8e4925c

Merge branch 'master' into mans0954/bipolar-theorem

6e69ff6

Merge branch 'master' into mans0954/polar_AbsConvex

c968034

Merge branch 'master' into mans0954/bipolar-theorem

312c8ad

Update Mathlib/Analysis/LocallyConvex/Basic.lean

cd6d3fa

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Fix

b8c3a7e

Merge branch 'mans0954/polar_AbsConvex' into mans0954/bipolar-theorem

8ae80b3

Get it building again

af0c3ff

Better

dc1aa39

Merge branch 'mans0954/polar_AbsConvex' into mans0954/bipolar-theorem

6e1d3a3

Build with sorry

9c5c169

Merge branch 'master' into mans0954/bipolar-theorem

326c14b

Pin down sorry

db6173c

weaken absConvexHull_zero_mem hypothesis

64eb847

j-loreaux added 3 commits March 23, 2026 11:14

try to fix

b23db5e

mk_all

1483008

Merge branch 'master' into mans0954/bipolar-theorem

c94a48d

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 23, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 5, 2026

themathqueen reviewed Apr 5, 2026

View reviewed changes

j-loreaux added 3 commits April 15, 2026 11:26

some minor fixes

6f5ecb6

Merge branch 'master' into mans0954/bipolar-theorem

fb0ebbb

try to simplify down to only new material. Don't move existing material.

d939239

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 15, 2026

j-loreaux added 4 commits April 15, 2026 13:01

remove the defeq abuse!

7899872

docstring

8493c1c

revert a file because the result already exists

061d6f6

move and clean up

4aad30d

github-actions Bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Apr 15, 2026

eric-wieser reviewed Apr 15, 2026

View reviewed changes

Comment thread Mathlib/Topology/Algebra/Module/Spaces/WeakBilin.lean Outdated

j-loreaux added 3 commits April 15, 2026 13:24

remove noncomputable

14682b3

mk_all

210e5a9

more clean-up

93f5787

j-loreaux removed awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. please-adopt Inactive PR (would be valuable to adopt) labels Apr 15, 2026

faenuccio reviewed Apr 19, 2026

View reviewed changes

faenuccio added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Apr 19, 2026

raresbuhai mentioned this pull request Oct 17, 2026

[Merged by Bors] - feat: prove the bipolar theorem for locally convex spaces TauCetiProject/TauCeti#17829

Closed

	lemma dualEmbedding_injective_of_separatingRight {E F : Type*} [AddCommGroup E] [AddCommGroup F]
	lemma eval_injective_of_separatingRight {E F : Type*} [AddCommGroup E] [AddCommGroup F]

	/-- The canonical linear equivalence (over `𝕝`) between `WeakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)`
	/-- The linear equivalence (over `𝕝`) between `WeakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)`

	c.f. `closureOperator_polar_gc_nonempty` below.
	cf. `closureOperator_polar_gc_nonempty` below.

	-- `0` is in `(closedAbsConvexHull 𝕜) s` so `u` must be strictly positive
	-- `0` is in `(closedAbsConvexHull 𝕜) s` so `u` must be strictly positive.

	-- Rescale `f` as `g` in order that for all `a` in `(closedAbsConvexHull 𝕜) s` `Re (g a) < 1`
	-- Rescale `f` as `g` in order that for all `a` in `(closedAbsConvexHull 𝕜) s` `Re (g a) < 1`.

	-- The dual embedding is surjective, let `f₀` be the element of `F` corresponding to `g`
	-- The dual embedding is surjective, let `f₀` be the element of `F` corresponding to `g`:

	-- Then, by construction, `f₀` is in the polar of `s`
	-- Then, by construction, `f₀` is in the polar of `s`.

Conversation

mans0954 commented Jun 24, 2025 • edited by faenuccio Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

j-loreaux commented Mar 23, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Apr 5, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

faenuccio left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

faenuccio Apr 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

j-loreaux commented Apr 23, 2026

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

12 participants

mans0954 commented Jun 24, 2025 •

edited by faenuccio

Loading

faenuccio Apr 19, 2026 •

edited

Loading