[Merged by Bors] - feat: port MeasureTheory.Function.ConvergenceInMeasure

[int-y1]

---

todo:

• TendstoInMeasure.exists_seq_tendsto_ae errors with number types and ^

[xroblot]

This one is a bit more tricky. There is currently a bug in Mathlib4 so that terms like r ^ n with r : ℝ and n : ℕ are changed automatically to r ^ (n : ℝ), see this issue

The way to fix that (at the moment) is to add the line

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

but then in any power of the form a ^ n with a : ℕ and n a negative integer fails because Lean does not to which type to cast a thus you need to give it the cast explicitly, say (a : ℝ) ^ n. In some cases, the correct type is not ℝ. In this file, it is ℝ≥0∞ at some places. You need to look at what happens in Lean3 for this file to figure out the correct type to use.

[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