[Merged by Bors] - feat(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull #17029

mans0954 · 2024-09-22T13:21:34Z

Defines the absolutely convex (or disked) hull of a subset of a locally convex space and proves a number of standard properties, including:

(subject to suitable conditions) the absolutely convex hull equals the convex hull of the balanced hull.
In a real vector space the absolutely convex hull of s equals the convex hull of s ∪ -s

depends on: [Merged by Bors] - feat(Algebra/Group/Pointwise/Set/Basic): sInter and sUnion forms of pointwise operations #17253

github-actions · 2024-09-22T13:22:16Z

PR summary 8d559b438f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ AbsConvex
+ AbsConvex.absConvexHull_eq
+ AbsConvex.absConvexHull_subset_iff
+ AbsConvex.empty
+ AbsConvex.iInter
+ AbsConvex.inter
+ AbsConvex.sInter
+ AbsConvex.univ
+ Balanced.sInter
+ _
+ absConvexHull
+ absConvexHull_add_subset
+ absConvexHull_empty
+ absConvexHull_eq_convexHull_balancedHull
+ absConvexHull_eq_empty
+ absConvexHull_eq_iInter
+ absConvexHull_eq_self
+ absConvexHull_min
+ absConvexHull_mono
+ absConvexHull_nonempty
+ absConvexHull_univ
+ absConvex_absConvexHull
+ balancedHull_add_subset
+ balancedHull_convexHull_subseteq_absConvexHull
+ balancedHull_mono
+ balancedHull_subset_convexHull_union_neg
+ balanced_absConvexHull
+ convexHull_union_neg_eq_absConvexHull
+ convex_absConvexHull
+ mem_absConvexHull_iff
+ nhds_hasBasis_absConvex
+ nhds_hasBasis_absConvex_open
+ subset_absConvexHull
+ ⟨_,
- nhds_basis_abs_convex
- nhds_basis_abs_convex_open

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Mathlib/Analysis/LocallyConvex/AbsConvex.lean

YaelDillies · 2024-09-28T11:09:30Z

Mathlib/Analysis/LocallyConvex/AbsConvex.lean

+
+variable {𝕜}
+
+theorem absConvex_empty : AbsConvex 𝕜 (∅ : Set E) := ⟨balanced_empty, convex_empty⟩


Suggested change

theorem absConvex_empty : AbsConvex 𝕜 (∅ : Set E) := ⟨balanced_empty, convex_empty⟩

theorem AbsConvex.empty : AbsConvex 𝕜 (∅ : Set E) := ⟨balanced_empty, convex_empty⟩

for dot notation. Same below. Feel free to open PRs to align the Balanced and Convex API to that new convention, btw

Mathlib/Analysis/LocallyConvex/AbsConvex.lean

Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

…ointwise operations (#17253) Provides `sInter` and `sUnion` versions of pointwise algebraic operations on sets. Needed in #17029 Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

Mathlib/Analysis/LocallyConvex/AbsConvex.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

YaelDillies

Thanks!

maintainer merge

github-actions · 2024-10-11T08:29:09Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

jcommelin

Thanks 🎉

bors merge

…Hull (#17029) Defines the absolutely convex (or disked) hull of a subset of a locally convex space and proves a number of standard properties, including: - (subject to suitable conditions) the absolutely convex hull equals the convex hull of the balanced hull. - In a real vector space the absolutely convex hull of `s` equals the convex hull of `s ∪ -s` Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

mathlib-bors · 2024-10-17T07:52:48Z

Pull request successfully merged into master.

Build succeeded:

… a single ring of scalars (#29342) Currently the definition of Absolutely Convex in Mathlib is a little unexpected: ``` def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s ``` At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`. Recently the requirements for the definition of `Convex` have been relaxed (#24392, #20595) so it is now possible to use a single scalar ring in common with the literature. Previous discussion: - #17029 (comment) - #26345 (comment)

mans0954 added 3 commits September 22, 2024 13:39

smul_set_sInter_subset

0032ca4

balanced_sInter

2a6ff0b

Define absolute convex hull and prove basic properties

fb7f025

mans0954 added the t-analysis Analysis (normed *, calculus) label Sep 22, 2024

mans0954 added 7 commits September 22, 2024 14:28

Update docstring

e25b80d

absConvexHull_eq_convexHull_union_neg

d0b4f4e

AbsConvex.hullAdd

6144bd1

Balanced.hullAdd

d3a9936

Tidy argument

141ab0f

Merge branch 'master' into mans0954/absconvexhull

9e921c7

Use AbsConvex in nhds theorems

a2c053e

mans0954 mentioned this pull request Sep 28, 2024

[Merged by Bors] - feature(Analysis/LocallyConvex/AbsConvex): The absolutely convex hull of a totally bounded set is totally bounded #17204

Closed

1 task

YaelDillies reviewed Sep 28, 2024

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 28, 2024

YaelDillies changed the title ~~feature(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull~~ feat(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull Sep 28, 2024

mans0954 and others added 14 commits September 28, 2024 12:27

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

bec008b

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

81f67b5

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

ac810da

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Use dot notation

2564767

Dot notation

265305d

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

50ae763

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Remove brackets

0bc891d

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

696dd9f

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

fce14a6

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

68ac073

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

51df29e

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

409a828

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Fix

34b1c88

Make convexHull_union_neg_eq_absConvexHull simp

d06e35b

mans0954 and others added 5 commits October 1, 2024 08:54

univ not Set.univ

cc6b861

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

1eb1dae

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

11a8e81

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Fix

dad37b3

Merge branch 'master' into mans0954/absconvexhull

4248c8c

mans0954 added 3 commits October 5, 2024 14:35

Merge branch 'master' into mans0954/absconvexhull

c26eeb4

Explain our choice of semirings

58d5b5a

Move to Implementation notes

93a4351

mans0954 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 5, 2024

Merge branch 'master' into mans0954/absconvexhull

4d0f481

YaelDillies reviewed Oct 11, 2024

View reviewed changes

Mathlib/Analysis/LocallyConvex/AbsConvex.lean Outdated Show resolved Hide resolved

Mathlib/Analysis/LocallyConvex/AbsConvex.lean Outdated Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 11, 2024

mans0954 and others added 3 commits October 11, 2024 09:14

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

e2c4c21

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Analysis/LocallyConvex/AbsConvex.lean

0bbb0f2

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Expand docstring

8d559b4

mans0954 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 11, 2024

YaelDillies approved these changes Oct 11, 2024

View reviewed changes

github-actions bot added the maintainer-merge label Oct 11, 2024

jcommelin reviewed Oct 17, 2024

View reviewed changes

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Oct 17, 2024

mathlib-bors bot changed the title ~~feat(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull~~ [Merged by Bors] - feat(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull Oct 17, 2024

mathlib-bors bot closed this Oct 17, 2024

mathlib-bors bot deleted the mans0954/absconvexhull branch October 17, 2024 07:52

mans0954 mentioned this pull request Aug 20, 2025

feat(Analysis/LocallyConvex/Polar): Bipolar theorem #26345

Open

1 task

mans0954 mentioned this pull request Sep 4, 2025

[Merged by Bors] - refactor(Analysis/LocallyConvex/AbsConvex): Redefine AbsConvex to use a single ring of scalars #29342

Closed

1 task


		variable {𝕜}

		theorem absConvex_empty : AbsConvex 𝕜 (∅ : Set E) := ⟨balanced_empty, convex_empty⟩

	theorem absConvex_empty : AbsConvex 𝕜 (∅ : Set E) := ⟨balanced_empty, convex_empty⟩
	theorem AbsConvex.empty : AbsConvex 𝕜 (∅ : Set E) := ⟨balanced_empty, convex_empty⟩

[Merged by Bors] - feat(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull #17029

[Merged by Bors] - feat(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull #17029

Uh oh!

Conversation

mans0954 commented Sep 22, 2024 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 22, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8d559b438f

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

YaelDillies Sep 28, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Oct 11, 2024

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Oct 17, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

mans0954 commented Sep 22, 2024 •

edited by YaelDillies

Loading

github-actions bot commented Sep 22, 2024 •

edited

Loading