[Merged by Bors] - feat: add some lemmas for Haar measures by xroblot · Pull Request #7034 · leanprover-community/mathlib4

xroblot · 2023-09-08T11:48:40Z

We prove some lemmas that will be useful in following PRs #6832 and #7037, mainly:

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

Mathlib/MeasureTheory/Measure/Haar/Basic.lean

Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

Mathlib/MeasureTheory/Measure/Haar/Basic.lean

Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Mathlib/MeasureTheory/Measure/Haar/Basic.lean

ADedecker

Thanks!

bors d+

Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

bors · 2023-09-11T19:21:23Z

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

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

xroblot · 2023-09-12T06:02:38Z

bors r+

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 · 2023-09-12T07:58:08Z

Build failed (retrying...):

Build

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 · 2023-09-12T08:18:10Z

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.

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>

xroblot added 2 commits September 8, 2023 13:47

1st commit

1766342

Clean up

01b073e

xroblot added WIP Work in progress t-measure-probability Measure theory / Probability theory awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Sep 8, 2023

Whitespace

f4fd951

xroblot mentioned this pull request Sep 8, 2023

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

Closed

1 task

xroblot changed the title ~~Add some lemmas for Haar measures~~ feat: add some lemmas for Haar measures Sep 8, 2023

xroblot mentioned this pull request Sep 8, 2023

[Merged by Bors] - feat: Prove that the measure equivalence between EuclideanSpace ℝ ι and ι → ℝ is volume preserving #7037

Closed

1 task

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 8, 2023

xroblot added awaiting-review and removed WIP Work in progress labels Sep 8, 2023