Skip to content

[Merged by Bors] - feat: fun_prop lemmas for GL n R and SL n R#37604

Closed
j-loreaux wants to merge 8 commits intoleanprover-community:masterfrom
j-loreaux:fun_prop-SL-GL
Closed

[Merged by Bors] - feat: fun_prop lemmas for GL n R and SL n R#37604
j-loreaux wants to merge 8 commits intoleanprover-community:masterfrom
j-loreaux:fun_prop-SL-GL

Conversation

@j-loreaux
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux commented Apr 3, 2026 •
edited
Loading

These lemmas allow fun_prop to prove that evaluating a continuous function into the general or special linear groups at an entry is continuous.

This also adds fun_prop to UpperHalfPlane.{num,denom}, Continuous.matrixVecCons and and new lemma Continuous.matrixOf and uses all these to golf some proofs of continuity regarding the action of SL 2 ℝ on ℍ from a recent PR.

For good measure, we add fun_prop to a number of other lemmas which should be tagged.

Closes #37472

Open in Gitpod

@j-loreaux j-loreaux requested a review from loefflerd April 3, 2026 16:46
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 3, 2026 •
edited
Loading

PR summary 7d837a8020

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Continuous.matrixOf
+ continuous_matrixOf
+ denom_continuous
+ num_continuous
++ continuous_apply

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).

j-loreaux
j-loreaux commented Apr 3, 2026
View reviewed changes
loefflerd
loefflerd reviewed Apr 3, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@loefflerd loefflerd left a comment

Choose a reason for hiding this comment

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

This is a great improvement, thanks! It's a pity it conflicts with #37601 but there's no way that could have been avoided (I opened that a matter of minutes ago).

j-loreaux
j-loreaux commented Apr 3, 2026
View reviewed changes
@j-loreaux j-loreaux added awaiting-author A reviewer has asked the author a question or requested changes. t-topology Topological spaces, uniform spaces, metric spaces, filters labels Apr 3, 2026
@j-loreaux j-loreaux removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 4, 2026
loefflerd
loefflerd reviewed Apr 4, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@loefflerd loefflerd left a comment

Choose a reason for hiding this comment

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

This looks great now!

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 4, 2026

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

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 4, 2026
@loefflerd loefflerd self-assigned this Apr 4, 2026
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Apr 4, 2026

!radar

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 4, 2026 •
edited
Loading

Benchmark results for 87cb564 against 7d837a8 are in. There are no significant changes. @loefflerd @riccardobrasca

  • 🟥 build//instructions: +36.9G (+0.02%)

Small changes (2🟥)

  • 🟥 build/module/Mathlib.LinearAlgebra.Alternating.Curry//instructions: +237.5M (+2.98%)
  • 🟥 build/module/Mathlib.Tactic.CasesM//instructions: +272.0M (+4.88%)

@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Apr 4, 2026

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 4, 2026

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 4, 2026
@j-loreaux
Copy link
Copy Markdown
Contributor Author

j-loreaux commented Apr 4, 2026

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Apr 4, 2026
@j-loreaux
feat: fun_prop lemmas for GL n R and SL n R (#37604)
53f40a8 
These lemmas allow `fun_prop` to prove that evaluating a continuous function into the general or special linear groups at an entry is continuous.

This also adds `fun_prop` to `UpperHalfPlane.{num,denom}`, `Continuous.matrixVecCons` and and new lemma `Continuous.matrixOf` and uses all these to golf some proofs of continuity regarding the action of `SL 2 ℝ` on `ℍ` from a recent PR.

For good measure, we add `fun_prop` to a number of other lemmas which should be tagged.

Closes #37472
@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Apr 4, 2026
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 4, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: fun_prop lemmas for GL n R and SL n R [Merged by Bors] - feat: fun_prop lemmas for GL n R and SL n R Apr 4, 2026
@mathlib-bors mathlib-bors bot closed this Apr 4, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@loefflerd loefflerd loefflerd left review comments

Assignees

@loefflerd loefflerd

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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.

fun_prop doesn't work well with matrix-valued functions

5 participants

@j-loreaux @riccardobrasca @leanprover-radar @sgouezel @loefflerd