Skip to content

[Merged by Bors] - feat: add mulEquivHaarChar#25829

Closed
kbuzzard wants to merge 5 commits intoleanprover-community:masterfrom
kbuzzard:kbuzzard-mulEquivHaarChar
Closed

[Merged by Bors] - feat: add mulEquivHaarChar#25829
kbuzzard wants to merge 5 commits intoleanprover-community:masterfrom
kbuzzard:kbuzzard-mulEquivHaarChar

Conversation

@kbuzzard
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard commented Jun 12, 2025 •
edited
Loading

API for the positive real factor by which an continuous multiplicative equivalence scales a regular Haar measure on a locally compact topological group.

From FLT.

Open in Gitpod

@github-actions github-actions bot added the t-measure-probability Measure theory / Probability theory label Jun 12, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 12, 2025 •
edited
Loading

PR summary 079d907947

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (new file) 2171

Declarations diff

+ IsHaarMeasure.nnreal_smul
+ haarScalarFactor_smul_smul
+ integral_comap_eq_mulEquivHaarChar_smul
+ mulEquivHaarChar
+ mulEquivHaarChar_eq
+ mulEquivHaarChar_pos
+ mulEquivHaarChar_refl
+ mulEquivHaarChar_smul_eq_comap
+ mulEquivHaarChar_smul_integral_map
+ mulEquivHaarChar_smul_map
+ mulEquivHaarChar_smul_preimage
+ mulEquivHaarChar_trans
+ mul_haarScalarFactor_smul

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

This was referenced Jun 14, 2025
Merged
Closed
RemyDegenne
RemyDegenne reviewed Jul 28, 2025
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! Sorry for the very long wait!

@RemyDegenne RemyDegenne added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 28, 2025
@kbuzzard kbuzzard added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Aug 1, 2025
@kbuzzard kbuzzard removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 1, 2025
EtienneC30
EtienneC30 reviewed Aug 3, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@EtienneC30 EtienneC30 left a comment

Choose a reason for hiding this comment

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

That's great!

@EtienneC30 EtienneC30 added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 3, 2025
@kbuzzard kbuzzard removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 4, 2025
EtienneC30
EtienneC30 reviewed Aug 4, 2025
View reviewed changes
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 4, 2025

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

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 4, 2025
@RemyDegenne
Copy link
Copy Markdown
Contributor

RemyDegenne commented Aug 5, 2025

Thanks!
bors r+

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 5, 2025
mathlib-bors bot pushed a commit that referenced this pull request Aug 5, 2025
@kbuzzard
feat: add mulEquivHaarChar (#25829)
8a90bb8 
API for the positive real factor by which an continuous multiplicative equivalence scales a regular Haar measure on a locally compact topological group. 

From FLT.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 5, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: add mulEquivHaarChar [Merged by Bors] - feat: add mulEquivHaarChar Aug 5, 2025
@mathlib-bors mathlib-bors bot closed this Aug 5, 2025
Equilibris pushed a commit to Equilibris/mathlib4 that referenced this pull request Aug 7, 2025
@kbuzzard
feat: add mulEquivHaarChar (leanprover-community#25829)
b0656f0 
API for the positive real factor by which an continuous multiplicative equivalence scales a regular Haar measure on a locally compact topological group. 

From FLT.
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@kbuzzard @Paul-Lez
feat: add mulEquivHaarChar (leanprover-community#25829)
3cba87e 
API for the positive real factor by which an continuous multiplicative equivalence scales a regular Haar measure on a locally compact topological group. 

From FLT.
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@kbuzzard @Paul-Lez
feat: add mulEquivHaarChar (leanprover-community#25829)
b844739 
API for the positive real factor by which an continuous multiplicative equivalence scales a regular Haar measure on a locally compact topological group. 

From FLT.
@dwrensha dwrensha mentioned this pull request Nov 30, 2025
Merged
kbuzzard pushed a commit to ImperialCollegeLondon/FLT that referenced this pull request Dec 3, 2025
@dwrensha
chore: remove upstreamed theorems in HaarChar/AddEquiv.lean (#780)
6668965 
In leanprover-community/mathlib4#25829,

*
[`mul_haarScalarFactor_smul`](https://github.com/ImperialCollegeLondon/FLT/blob/a65b8df3077496740f4fea21edab267ab5928f5e/FLT/HaarMeasure/HaarChar/AddEquiv.lean#L45)
was upstreamed as
[`MeasureTheory.Measure.mul_haarScalarFactor_smul`](https://github.com/leanprover-community/mathlib4/blob/b86f640b984928b1185ddc3cc5686f993a1f109f/Mathlib/MeasureTheory/Measure/Haar/Unique.lean#L350-L370)
*
[`haarScalarFactor_smul_smul`](https://github.com/ImperialCollegeLondon/FLT/blob/a65b8df3077496740f4fea21edab267ab5928f5e/FLT/HaarMeasure/HaarChar/AddEquiv.lean#L68)
was upstreamed as
[`MeasureTheory.Measure.haarScalarFactor_smul_smul`](https://github.com/leanprover-community/mathlib4/blob/b86f640b984928b1185ddc3cc5686f993a1f109f/Mathlib/MeasureTheory/Measure/Haar/Unique.lean#L372-L378)
*
[`mulEquivHaarChar_map`](https://github.com/ImperialCollegeLondon/FLT/blob/a65b8df3077496740f4fea21edab267ab5928f5e/FLT/HaarMeasure/HaarChar/AddEquiv.lean#L94)
was upstreamed as [`MeasureTheory.mulEquivHaarChar_smul_map
`](https://github.com/leanprover-community/mathlib4/blob/b86f640b984928b1185ddc3cc5686f993a1f109f/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean#L62-L68)
*
[`mulEquivHaarChar_comap`](https://github.com/ImperialCollegeLondon/FLT/blob/a65b8df3077496740f4fea21edab267ab5928f5e/FLT/HaarMeasure/HaarChar/AddEquiv.lean#L113)
was upstreamed as
[`MeasureTheory.mulEquivHaarChar_smul_eq_comap`](https://github.com/leanprover-community/mathlib4/blob/b86f640b984928b1185ddc3cc5686f993a1f109f/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean#L70-L80)
*
[`mulEquivHaarChar_smul_integral_comap`](https://github.com/ImperialCollegeLondon/FLT/blob/a65b8df3077496740f4fea21edab267ab5928f5e/FLT/HaarMeasure/HaarChar/AddEquiv.lean#L125)
was upstreamed as
[`MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul`](https://github.com/leanprover-community/mathlib4/blob/b86f640b984928b1185ddc3cc5686f993a1f109f/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean#L89-L101)
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

@EtienneC30 EtienneC30 EtienneC30 left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kbuzzard @RemyDegenne @EtienneC30