[Merged by Bors] - feat: port MeasureTheory.Measure.Lebesgue.Basic

[Komyyy]

---

[hrmacbeth]

Have stopped for now.

[Komyyy]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/MeasureTheory.2EMeasure.2ELebesgue.2EBasic.20!4.234552
In Lean 4, the following tc search fails, even if we make volume reducible in MeasureSpaceDef.

variable [Fintype ι]
#synth SigmaFinite (volume : Measure (ι → ℝ))
-- fails
#synth SigmaFinite (Measure.pi fun _ => volume : Measure (ι → ℝ))
-- defeq and succeeds
#synth AddLeftInvariant (volume : Measure (ι → ℝ))
-- fails
#synth AddLeftInvariant (Measure.pi fun _ => (stdOrthonormalBasis ℝ ℝ).toBasis.addHaar : Measure (ι → ℝ))
-- defeq and succeeds

These instances are required in this file.
This file can be built by specifying latter measures now, but this should be fixed clearly.
Does anyone know how to fix this?

[Komyyy]

At the moment, I added the porting note of this problem and continue porting.

[jcommelin]

Thanks 🎉

bors merge

[bors]

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.

• Build
• Check all files imported
• Lint style