Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: Amenable monoid actions #7395

Open
wants to merge 33 commits into
base: master
Choose a base branch
from
Open

feat: Amenable monoid actions #7395

wants to merge 33 commits into from
+106 −0

Conversation

matthias567
Copy link
Collaborator

@matthias567 matthias567 commented Sep 27, 2023 •
edited by eric-wieser
Loading

Open in Gitpod

@matthias567 matthias567 added the awaiting-review The author would like community review of the PR label Sep 27, 2023
github-actions[bot]
github-actions bot reviewed Sep 27, 2023
View reviewed changes
docs/references.bib Outdated Show resolved Hide resolved
sgouezel
sgouezel reviewed Sep 27, 2023
View reviewed changes
Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated Show resolved Hide resolved
matthias567 and others added 3 commits September 27, 2023 12:25
@matthias567 @sgouezel
fix typo
936d3aa 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@matthias567 @sgouezel
remove space
5be029a 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@matthias567
replace ENNReal by NNReal
c11a5a7
@matthias567 matthias567 added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 27, 2023
@matthias567 matthias567 added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 28, 2023
YaelDillies
YaelDillies reviewed Sep 28, 2023
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

What about redefining ProbabilityMeasure as extending both Measure and Mean? (mostly a question for the resident measure theorists)

Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated Show resolved Hide resolved
matthias567 and others added 2 commits September 28, 2023 11:14
@matthias567 @YaelDillies
rename fields of Mean
f48cfac 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@matthias567
fix names of fields in Mean
12a13ff
matthias567 and others added 5 commits October 16, 2023 21:05
@matthias567 @eric-wieser
remove - in block comment
17ed9ab 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@matthias567 @eric-wieser
finadd: arguments before colon
8667af4 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@matthias567 @eric-wieser
Make Proposition TitleCase
a78f94b 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@matthias567
cut line to 100 chars
0e38763
@matthias567
TitleCase
a0bb466
@sgouezel sgouezel added the new-contributor This PR was made by a contributor with fewer than 5 merged PRs. Welcome to the community! label Nov 5, 2023
sgouezel
sgouezel reviewed Nov 8, 2023
View reviewed changes
Copy link
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

Sorry for the review delay. Overall, this looks good to me, although I have minor nitpicky comments (which is perfectly normal).

Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated


/-- For amenable actions, we can pick an invariant mean -/
noncomputable def invmean_of_amenable (h: Amenable α G) :
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
noncomputable def invmean_of_amenable (h: Amenable α G) :
noncomputable def invariantMean_of_amenable (h : Amenable α G) :

If you have made Amenable a typeclass, though, I would change this to invMean [Amenable α G], where the difference would be necessary to emphasize that it's not the same thing (i.e., we are picking some choice, vs. the space of all invariant means).

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes, I'll do this. However, this breaks invMean. I might need some help in fixing that (in the commit #8b3e8d7de, this is the comment at the end of the file)

Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/GroupAction/Amenable.lean Outdated Show resolved Hide resolved
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes t-measure-probability Measure theory / Probability theory t-dynamics Dynamical Systems and removed awaiting-review The author would like community review of the PR labels Nov 8, 2023
@matthias567 matthias567 added bug Something isn't working help-wanted The author needs attention to resolve issues awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes bug Something isn't working labels Nov 14, 2023
@YaelDillies YaelDillies changed the title feat(GroupTheory/GroupActions/amenable): add definition of amenable monoid actions feat: Amenable monoid actions Nov 14, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

@github-actions github-actions[bot] github-actions left review comments

@ADedecker ADedecker Awaiting requested review from ADedecker

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

@sgouezel sgouezel Awaiting requested review from sgouezel

Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR help-wanted The author needs attention to resolve issues merge-conflict The PR has a merge conflict with master, and needs manual merging. new-contributor This PR was made by a contributor with fewer than 5 merged PRs. Welcome to the community! t-dynamics Dynamical Systems t-measure-probability Measure theory / Probability theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@matthias567 @ADedecker @eric-wieser @sgouezel @YaelDillies @leanprover-community-mathlib4-bot @JLimperg