Skip to content

[Merged by Bors] - feat: f is lowersemicontinuous iff -f is uppersemicontinuous#36598

Closed
CoolRmal wants to merge 9 commits intoleanprover-community:masterfrom
CoolRmal:upperSemiContinuousNeg
Closed

[Merged by Bors] - feat: f is lowersemicontinuous iff -f is uppersemicontinuous#36598
CoolRmal wants to merge 9 commits intoleanprover-community:masterfrom
CoolRmal:upperSemiContinuousNeg

Conversation

@CoolRmal
Copy link
Copy Markdown
Contributor

@CoolRmal CoolRmal commented Mar 13, 2026

Proved that a function f is lowersemicontinuous iff -f is uppersemicontinuous. Also changed the hypothesis of upperSemicontinuousOn_iff_preimage_Iio from LinearOrder to Preorder.

Used in the proof of conditional Jensen's inequality for concave functions.

Open in Gitpod

@CoolRmal CoolRmal mentioned this pull request Mar 13, 2026
Closed
4 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 13, 2026 •
edited
Loading

PR summary 80ba5bde21

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ LowerSemicontinuous.inv
+ LowerSemicontinuousAt.inv
+ LowerSemicontinuousOn.inv
+ LowerSemicontinuousWithinAt.inv
+ UpperSemicontinuous.inv
+ UpperSemicontinuousAt.inv
+ UpperSemicontinuousOn.inv
+ UpperSemicontinuousWithinAt.inv
+ lowerSemiContinuous_inv_iff
+ lowerSemicontinuouAt_inv_iff
+ lowerSemicontinuousOn_inv_iff
+ lowerSemicontinuousWithinAt_inv_iff
+ upperSemiContinuous_inv_iff
+ upperSemicontinuousAt_inv_iff
+ upperSemicontinuousOn_inv_iff
+ upperSemicontinuousWithinAt_inv_iff

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

themathqueen
themathqueen reviewed Mar 13, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Notation/Pi/Defs.lean Outdated
themathqueen
themathqueen reviewed Mar 13, 2026
View reviewed changes
Comment thread Mathlib/Topology/Semicontinuity/Basic.lean Outdated
@themathqueen themathqueen added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Mar 13, 2026
j-loreaux
j-loreaux reviewed Mar 13, 2026
View reviewed changes
Comment thread Mathlib/Topology/Semicontinuity/Basic.lean
Comment on lines -877 to +885
variable {β : Type*} [LinearOrder β]
variable {β : Type*}
variable {γ : Type*} [TopologicalSpace γ]
variable {f : α → β} {g : γ → α} {s : Set α} {a : α} {c : γ} {t : Set γ}

theorem upperSemicontinuousOn_iff_preimage_Iio :
theorem upperSemicontinuousOn_iff_preimage_Iio [Preorder β] :
UpperSemicontinuousOn f s ↔ ∀ b, ∃ u : Set α, IsOpen u ∧ s ∩ f ⁻¹' Set.Iio b = s ∩ u :=
lowerSemicontinuousOn_iff_preimage_Ioi (β := βᵒᵈ)

theorem upperSemicontinuousOn_iff_preimage_Ici :
theorem upperSemicontinuousOn_iff_preimage_Ici [LinearOrder β] :
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux Mar 13, 2026

Choose a reason for hiding this comment

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

I think this serves no purpose right now. If you really need upper semicontinuous functions on preorder, then a larger refactor is in order.

Copy link
Copy Markdown
Contributor Author

@CoolRmal CoolRmal Mar 14, 2026

Choose a reason for hiding this comment

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

I made this change because lowerSemicontinuous_iff_isOpen_preimage only requires [Preorder β].

Comment thread Mathlib/Topology/Semicontinuity/Basic.lean Outdated
@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 13, 2026
@CoolRmal
Copy link
Copy Markdown
Contributor Author

CoolRmal commented Mar 14, 2026

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 14, 2026
RemyDegenne
RemyDegenne reviewed Mar 17, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Notation/Pi/Defs.lean Outdated
@RemyDegenne
Copy link
Copy Markdown
Contributor

RemyDegenne commented Mar 17, 2026

Thanks!
bors r+

mathlib-bors bot pushed a commit that referenced this pull request Mar 17, 2026
@CoolRmal
feat: f is lowersemicontinuous iff -f is uppersemicontinuous (#36598)
310419d 
Proved that a function `f` is lowersemicontinuous iff `-f` is uppersemicontinuous. Also changed the hypothesis of `upperSemicontinuousOn_iff_preimage_Iio` from LinearOrder to Preorder.

Used in the proof of conditional Jensen's inequality for concave functions.
@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Mar 17, 2026
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 17, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: f is lowersemicontinuous iff -f is uppersemicontinuous [Merged by Bors] - feat: f is lowersemicontinuous iff -f is uppersemicontinuous Mar 17, 2026
@mathlib-bors mathlib-bors bot closed this Mar 17, 2026
@CoolRmal CoolRmal deleted the upperSemiContinuousNeg branch March 17, 2026 19:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@RemyDegenne RemyDegenne RemyDegenne left review comments

@j-loreaux j-loreaux j-loreaux left review comments

@themathqueen themathqueen themathqueen left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@CoolRmal @RemyDegenne @j-loreaux @themathqueen