Skip to content

[Merged by Bors] - feat(Analysis/Complex/UpperHalfPlane): SL(2, R) action is proper#36895

Closed
loefflerd wants to merge 30 commits intoleanprover-community:masterfrom
loefflerd:DL_properSMul
Closed

[Merged by Bors] - feat(Analysis/Complex/UpperHalfPlane): SL(2, R) action is proper#36895
loefflerd wants to merge 30 commits intoleanprover-community:masterfrom
loefflerd:DL_properSMul

Conversation

@loefflerd
Copy link
Copy Markdown
Contributor

@loefflerd loefflerd commented Mar 20, 2026 •
edited
Loading

Show that the actions of SL(2, ℝ) and GL(2, ℝ) on the upper half-plane are continuous in both variables, and the action of SL(2, ℝ) is proper.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

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

PR summary 1c98d2c008

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (new file) 2355

Declarations diff

+ IsPretransitive.of_orbit
+ absq_le
+ cdsq_le
+ coe_toSL2R
+ continuous_toSL2R
+ instContinuousSMulGL2R
+ instContinuousSMulSL2R
+ instProperSMul
+ isClosedEmbedding_val
+ isPretransitiveGL2R
+ isPretransitiveSL2R
+ isProperMap_smul_I
+ toSL2R
+ toSL2R_apply
+ toSL2R_smul_I
+ σ_eventuallyEq

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

@loefflerd loefflerd added the t-analysis Analysis (normed *, calculus) label Mar 20, 2026
ADedecker
ADedecker reviewed Mar 20, 2026
View reviewed changes
Comment thread Mathlib/Topology/Algebra/ProperAction/Fiberwise.lean Outdated
ADedecker
ADedecker reviewed Mar 20, 2026
View reviewed changes
Comment thread Mathlib/Topology/Algebra/ProperAction/Fiberwise.lean Outdated
ADedecker
ADedecker reviewed Mar 20, 2026
View reviewed changes
Comment thread Mathlib/Topology/Algebra/ProperAction/Fiberwise.lean Outdated
@ADedecker ADedecker added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 20, 2026
@loefflerd loefflerd mentioned this pull request Mar 20, 2026
Closed
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 20, 2026
@loefflerd loefflerd removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 20, 2026
@loefflerd
Copy link
Copy Markdown
Contributor Author

loefflerd commented Mar 22, 2026

For some strange reason this did not pass CI with a linter warning in some totally unrelated (AFAIK) code. I have merged latest master on #36904 and cascaded that through to here (but I don't understand why #36904 itself did pass the linter).

@loefflerd
Copy link
Copy Markdown
Contributor Author

loefflerd commented Mar 22, 2026

This PR seems to be cursed: whatever I do I get random CI failures. I'm just going to leave it be for now, and hope the bugs are gone once the upstream PR's it depends on are merged.

@mathlib-merge-conflicts 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 Mar 23, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 23, 2026

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

@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 Mar 24, 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 Mar 24, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 24, 2026

This PR/issue depends on:

j-loreaux
j-loreaux reviewed Mar 31, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux 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 very nice. My only complaint, and it is not a complaint against you, is that fun_prop can't be used to tackle these continuity goals. That makes me very sad. One problem at least is that it can't make use of Continuous.matrix_elem. I don't see an easy way to solve this.

bors d+

Comment thread Mathlib/Analysis/Complex/UpperHalfPlane/ProperAction.lean Outdated
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 31, 2026

✌️ loefflerd 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 the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 31, 2026
@loefflerd loefflerd mentioned this pull request Apr 1, 2026
Closed
@loefflerd
Copy link
Copy Markdown
Contributor Author

loefflerd commented Apr 1, 2026

Thanks Jireh for the review! I filed an issue, just so your comment doesn't get forgotten (about fun_prop not working as well as it might).

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Apr 1, 2026
@loefflerd
feat(Analysis/Complex/UpperHalfPlane): SL(2, R) action is proper (#36895
18a09f9 
)

Show that the actions of `SL(2, ℝ)` and `GL(2, ℝ)` on the upper half-plane are continuous in both variables, and the action of `SL(2, ℝ)` is proper.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 1, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Analysis/Complex/UpperHalfPlane): SL(2, R) action is proper [Merged by Bors] - feat(Analysis/Complex/UpperHalfPlane): SL(2, R) action is proper Apr 1, 2026
@mathlib-bors mathlib-bors bot closed this Apr 1, 2026
@loefflerd loefflerd deleted the DL_properSMul branch April 1, 2026 06:49
aditya-ramabadran pushed a commit to aditya-ramabadran/mathlib4 that referenced this pull request Apr 1, 2026
@loefflerd @aditya-ramabadran
feat(Analysis/Complex/UpperHalfPlane): SL(2, R) action is proper (lea…
3d42dff 
…nprover-community#36895)

Show that the actions of `SL(2, ℝ)` and `GL(2, ℝ)` on the upper half-plane are continuous in both variables, and the action of `SL(2, ℝ)` is proper.
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Apr 3, 2026
@loefflerd @xroblot
feat(Analysis/Complex/UpperHalfPlane): SL(2, R) action is proper (lea…
a3e015b 
…nprover-community#36895)

Show that the actions of `SL(2, ℝ)` and `GL(2, ℝ)` on the upper half-plane are continuous in both variables, and the action of `SL(2, ℝ)` is proper.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

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

@ADedecker ADedecker ADedecker left review comments

Assignees

@j-loreaux j-loreaux

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@loefflerd @j-loreaux @ADedecker