Skip to content

[Merged by Bors] - feat: a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space#31411

Closed
CoolRmal wants to merge 38 commits intoleanprover-community:masterfrom
CoolRmal:convexsup
Closed

[Merged by Bors] - feat: a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space#31411
CoolRmal wants to merge 38 commits intoleanprover-community:masterfrom
CoolRmal:convexsup

Conversation

@CoolRmal
Copy link
Copy Markdown
Contributor

@CoolRmal CoolRmal commented Nov 9, 2025 •
edited
Loading

In this PR we show that a convex lower-semicontinuous function is the upper envelope of a family
of continuous affine linear functions. We further prove that it is the upper envelope of countably many affine functions if the underlying space is Hereditarily Lindelof.

Special thanks to @ADedecker for pointing out Bourbaki’s proof, which greatly simplified my code, and to @RemyDegenne for his prompt reviews and helpful comments.

Open in Gitpod

@CoolRmal CoolRmal marked this pull request as ready for review November 9, 2025 07:44
@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Nov 9, 2025
@CoolRmal CoolRmal mentioned this pull request Nov 9, 2025
Closed
4 tasks
@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Nov 9, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 9, 2025 •
edited
Loading

PR summary a01c8cb529

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.Convex.Approximation (new file) 2006

Declarations diff

+ _root_.LowerSemicontinuousOn.isClosed_re_epigraph
+ convex_re_epigraph
+ exists_affine_le_of_lt
+ real_sSup_affine_eq
+ real_sSup_of_countable_affine_eq
+ real_sSup_of_nat_affine_eq
+ real_univ_sSup_affine_eq
+ real_univ_sSup_of_countable_affine_eq
+ real_univ_sSup_of_nat_affine_eq
+ sSup_affine_eq
+ sSup_of_countable_affine_eq
+ sSup_of_nat_affine_eq
+ univ_sSup_affine_eq
+ univ_sSup_of_countable_affine_eq
+ univ_sSup_of_nat_affine_eq

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 scripts/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 9, 2025
@CoolRmal CoolRmal mentioned this pull request Nov 11, 2025
Closed
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-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 Nov 19, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 19, 2025

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

@grunweg grunweg changed the title feat : a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space feat: a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space Nov 19, 2025
@github-actions 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 Feb 15, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 15, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Feb 15, 2026

This PR/issue depends on:

RemyDegenne
RemyDegenne reviewed Feb 15, 2026
View reviewed changes
RemyDegenne
RemyDegenne reviewed Feb 15, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@RemyDegenne RemyDegenne left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks good!

CoolRmal and others added 10 commits February 15, 2026 11:04
@CoolRmal
Update Approximation.lean
9a99e99
@CoolRmal @RemyDegenne
Update Mathlib/Analysis/Convex/Approximation.lean
099d6ad 
Co-authored-by: Rémy Degenne <[email protected]>
@CoolRmal @RemyDegenne
Update Mathlib/Analysis/Convex/Approximation.lean
ffed38a 
Co-authored-by: Rémy Degenne <[email protected]>
@CoolRmal @RemyDegenne
Update Mathlib/Analysis/Convex/Approximation.lean
8a1007f 
Co-authored-by: Rémy Degenne <[email protected]>
@CoolRmal @RemyDegenne
Update Mathlib/Analysis/Convex/Approximation.lean
45216d5 
Co-authored-by: Rémy Degenne <[email protected]>
@CoolRmal @RemyDegenne
Update Mathlib/Analysis/Convex/Approximation.lean
d39b1b1 
Co-authored-by: Rémy Degenne <[email protected]>
@CoolRmal @RemyDegenne
Update Mathlib/Analysis/Convex/Approximation.lean
3ee4c28 
Co-authored-by: Rémy Degenne <[email protected]>
@CoolRmal @RemyDegenne
Update Mathlib/Analysis/Convex/Approximation.lean
7479c29 
Co-authored-by: Rémy Degenne <[email protected]>
@CoolRmal @RemyDegenne
Update Mathlib/Analysis/Convex/Approximation.lean
b5e9892 
Co-authored-by: Rémy Degenne <[email protected]>
@CoolRmal @RemyDegenne
Update Mathlib/Analysis/Convex/Approximation.lean
ccf5dd4 
Co-authored-by: Rémy Degenne <[email protected]>
@RemyDegenne
Copy link
Copy Markdown
Contributor

RemyDegenne commented Feb 15, 2026

Could you update the PR description? Currently it talks about a file that you are not using anymore.

RemyDegenne
RemyDegenne approved these changes Feb 15, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@RemyDegenne RemyDegenne left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
bors r+

@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Feb 15, 2026
mathlib-bors bot pushed a commit that referenced this pull request Feb 15, 2026
@CoolRmal
feat: a convex lower-semicontinuous function is the supremum of a seq…
d2bb277 
…uence of affine functions in a separable space (#31411)

In this PR we show that a convex lower-semicontinuous function is the upper envelope of a family
of continuous affine linear functions. We further prove that it is the upper envelope of countably many affine functions if the underlying space is Hereditarily Lindelof.

Special thanks to @ADedecker  for pointing out Bourbaki’s proof, which greatly simplified my code, and to @RemyDegenne for his prompt reviews and helpful comments.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 15, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space [Merged by Bors] - feat: a convex lower-semicontinuous function is the supremum of a sequence of affine functions in a separable space Feb 15, 2026
@mathlib-bors mathlib-bors bot closed this Feb 15, 2026
@CoolRmal CoolRmal deleted the convexsup branch February 16, 2026 00:12
@CoolRmal CoolRmal mentioned this pull request Feb 17, 2026
Closed
1 task
Maldooor pushed a commit to Maldooor/mathlib4 that referenced this pull request Feb 25, 2026
@CoolRmal @Maldooor
feat: a convex lower-semicontinuous function is the supremum of a seq…
0f0c284 
…uence of affine functions in a separable space (leanprover-community#31411)

In this PR we show that a convex lower-semicontinuous function is the upper envelope of a family
of continuous affine linear functions. We further prove that it is the upper envelope of countably many affine functions if the underlying space is Hereditarily Lindelof.

Special thanks to @ADedecker  for pointing out Bourbaki’s proof, which greatly simplified my code, and to @RemyDegenne for his prompt reviews and helpful comments.
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Mar 2, 2026
@CoolRmal @pfaffelh
feat: a convex lower-semicontinuous function is the supremum of a seq…
f17f1b4 
…uence of affine functions in a separable space (leanprover-community#31411)

In this PR we show that a convex lower-semicontinuous function is the upper envelope of a family
of continuous affine linear functions. We further prove that it is the upper envelope of countably many affine functions if the underlying space is Hereditarily Lindelof.

Special thanks to @ADedecker  for pointing out Bourbaki’s proof, which greatly simplified my code, and to @RemyDegenne for his prompt reviews and helpful comments.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@RemyDegenne RemyDegenne RemyDegenne approved these changes

Assignees

No one assigned

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@CoolRmal @mathlib4-merge-conflict-bot @RemyDegenne @mathlib4-dependent-issues-bot