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

[Merged by Bors] - feat: remove the diamond for Complex.measureSpace #6832

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat: remove the diamond for Complex.measureSpace #6832

wants to merge 17 commits into from

Conversation

xroblot
Copy link
Collaborator

@xroblot xroblot commented Aug 28, 2023 •
edited
Loading

We remove the instance

instance measureSpace : MeasureSpace ℂ :=  ⟨Measure.map basisOneI.equivFun.symm volume⟩

in MeasureTheory.Measure.Lebesgue.Complex since ℂ has already a measureSpace instance coming from its InnerProductSpace structure over ℝ, and fix the proof of volume_preserving_equiv_pi.

Co-authored-by: Eric Wieser wieser.eric@gmail.com

Open in Gitpod

@xroblot xroblot added awaiting-CI t-measure-probability Measure theory / Probability theory labels Aug 28, 2023
@xroblot xroblot mentioned this pull request Aug 25, 2023
Closed
4 tasks
@xroblot xroblot added awaiting-review easy < 20s of review time. See the lifecycle page for guidelines. labels Aug 28, 2023
@xroblot xroblot mentioned this pull request Aug 31, 2023
Closed
3 tasks
eric-wieser
eric-wieser approved these changes Sep 2, 2023
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

LGTM

My only question is whether this is considered a "heavy" import, and if it should go in a new Haar.Complex file instead. I'll let another maintainer decide

maintainer merge.

@github-actions
Copy link

github-actions bot commented Sep 2, 2023

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

@sgouezel
Copy link
Contributor

sgouezel commented Sep 2, 2023

There is a problem with this file, that we have a diamond: complex numbers already have a measure space instance before the start of the file (you can try example : MeasureSpace ℂ := by infer_instance before the instance declaration) -- and this instance is already known to be a Haar measure (try example : Measure.IsAddHaarMeasure (@volume ℂ _) := by infer_instance). So instead of adding this new instance, we should fix the file and remove the diamond (by just removing the instance)

@eric-wieser
Copy link
Member

There is a problem with this file, that we have a diamond

Indeed, this is discussed here

@xroblot
Copy link
Collaborator Author

xroblot commented Sep 2, 2023

I see, so the plan is to remove the instance at the start of the file (then the Haar measure instance is synthesised automatically) and just come up with a new proof of volume_preserving_equiv_pi (and probably a new definition for measurableEquivPi first).

@xroblot xroblot added WIP Work in progress and removed awaiting-review easy < 20s of review time. See the lifecycle page for guidelines. labels Sep 3, 2023
@xroblot xroblot changed the title feat: add IsAddHaarMeasure instance for Complex.measureSpace feat: remove the diamond for Complex.measureSpace Sep 5, 2023
@xroblot xroblot added awaiting-review WIP Work in progress and removed awaiting-review labels Sep 5, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib label Sep 8, 2023
@xroblot xroblot mentioned this pull request Sep 8, 2023
Closed
@xroblot xroblot added awaiting-review and removed WIP Work in progress labels Sep 8, 2023
bors bot pushed a commit that referenced this pull request Sep 12, 2023
@xroblot @eric-wieser
feat: add some lemmas for Haar measures (#7034)
bbc0bc5 
We prove some lemmas that will be useful in following PRs #6832 and #7037, mainly:
```lean
theorem Basis.addHaar_eq {b : Basis ι ℝ E} {b' : Basis ι' ℝ E} :
     b.addHaar = b'.addHaar ↔ b.addHaar b'.parallelepiped = 1

theorem Basis.parallelepiped_eq_map (b : Basis ι ℝ E) :
     b.parallelepiped = (TopologicalSpace.PositiveCompacts.piIcc01 ι).map b.equivFun.symm
       b.equivFunL.symm.continuous

theorem Basis.addHaar_map (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) :
    map f b.addHaar = (b.map f.toLinearEquiv).addHaar
```

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
bors bot pushed a commit that referenced this pull request Sep 12, 2023
@xroblot @eric-wieser
feat: add some lemmas for Haar measures (#7034)
26bdb03 
We prove some lemmas that will be useful in following PRs #6832 and #7037, mainly:
```lean
theorem Basis.addHaar_eq {b : Basis ι ℝ E} {b' : Basis ι' ℝ E} :
     b.addHaar = b'.addHaar ↔ b.addHaar b'.parallelepiped = 1

theorem Basis.parallelepiped_eq_map (b : Basis ι ℝ E) :
     b.parallelepiped = (TopologicalSpace.PositiveCompacts.piIcc01 ι).map b.equivFun.symm
       b.equivFunL.symm.continuous

theorem Basis.addHaar_map (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) :
    map f b.addHaar = (b.map f.toLinearEquiv).addHaar
```

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Sep 12, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@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 Sep 12, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 12, 2023
@urkud
Copy link
Member

urkud commented Sep 16, 2023

Thanks! 🎉
bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 16, 2023
bors bot pushed a commit that referenced this pull request Sep 16, 2023
@xroblot @eric-wieser
feat: remove the diamond for Complex.measureSpace (#6832)
67b54e2 
We remove the instance 
```lean
instance measureSpace : MeasureSpace ℂ :=  ⟨Measure.map basisOneI.equivFun.symm volume⟩
```
in `MeasureTheory.Measure.Lebesgue.Complex` since `ℂ` has already a `measureSpace` instance coming from its `InnerProductSpace` structure over `ℝ`, and fix the proof of `volume_preserving_equiv_pi`.


Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Sep 16, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: remove the diamond for Complex.measureSpace [Merged by Bors] - feat: remove the diamond for Complex.measureSpace Sep 16, 2023
@bors bors bot closed this Sep 16, 2023
@bors bors bot deleted the xfr_complex_measure_ishaar branch September 16, 2023 01:19
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@xroblot @eric-wieser @kodyvajjha
feat: add some lemmas for Haar measures (#7034)
01a1e92 
We prove some lemmas that will be useful in following PRs #6832 and #7037, mainly:
```lean
theorem Basis.addHaar_eq {b : Basis ι ℝ E} {b' : Basis ι' ℝ E} :
     b.addHaar = b'.addHaar ↔ b.addHaar b'.parallelepiped = 1

theorem Basis.parallelepiped_eq_map (b : Basis ι ℝ E) :
     b.parallelepiped = (TopologicalSpace.PositiveCompacts.piIcc01 ι).map b.equivFun.symm
       b.equivFunL.symm.continuous

theorem Basis.addHaar_map (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) :
    map f b.addHaar = (b.map f.toLinearEquiv).addHaar
```

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@xroblot @eric-wieser @kodyvajjha
feat: remove the diamond for Complex.measureSpace (#6832)
f1aefbb 
We remove the instance 
```lean
instance measureSpace : MeasureSpace ℂ :=  ⟨Measure.map basisOneI.equivFun.symm volume⟩
```
in `MeasureTheory.Measure.Lebesgue.Complex` since `ℂ` has already a `measureSpace` instance coming from its `InnerProductSpace` structure over `ℝ`, and fix the proof of `volume_preserving_equiv_pi`.


Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

@sgouezel sgouezel Awaiting requested review from sgouezel

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.

None yet
5 participants
@xroblot @sgouezel @eric-wieser @leanprover-community-mathlib4-bot @urkud