MeasurableDiv for Complex and Real types

Stream: new members

[Marmare314]

Is there any reason why no complex or real type is an instance of MeasurableDiv\2? Since Division by zero is defined to be zero I think it should be possible to define this instance.
I am trying to prove that for every measurable complex function f there is a function g:=f / |f| such that |f|*g=f. Having this instance would make this really easy.

[Yaël Dillies]

You can try proving it!

[Marmare314]

Now that I looked at it in the way its stated in MeasurableDiv\2 I'm not even sure its true. And even less so how I could prove it in lean. It probably would need to be shown explicitly using the definition of measurability right?

[Henrik Rueping]

(deleted)

[Marmare314]

Ah well, apparently it wasn't that difficult after all

instance : MeasurableDiv₂ ℝ where
  measurable_div := by
    simp only [div_eq_mul_inv]
    exact Measurable.mul measurable_fst (Measurable.comp measurable_inv measurable_snd)

instance : MeasurableDiv₂ ℂ where
  measurable_div := by
    simp only [div_eq_mul_inv]
    exact Measurable.mul measurable_fst (Measurable.comp measurable_inv measurable_snd)

[Kevin Buzzard]

Does the measurability tactic not do these? @Tomas Skrivan are these goals good targets for fun_prop?

[Marmare314]

I don't think it does, but I rarely have success with aesop tactics unfortunately.

[Tomas Skrivan]

With fun_prop the proof would be simp only [div_eq_mul_inv]; fun_prop.

fun_prop can even infer measurability from continuity, see this example

However, it is not merged to the master branch yet. Scott Morrison do you know if anyone else is planning on reviewing it or can we merge it?

[Yaël Dillies]

Marmare314 said:

Ah well, apparently it wasn't that difficult after all [...]

You can actually make it a general MeasurableInv α → MeasurableMul₂ α → MeasurableDiv₂ α instance.

[Marmare314]

Something like this?

instance (G : Type*) [DivInvMonoid G] [MeasurableSpace G] [MeasurableInv G] [MeasurableMul₂ G] : MeasurableDiv₂ G where
  measurable_div := by simp only [div_eq_mul_inv]; measurability

(measurability actually does work after the simp only call)

[Kevin Buzzard]

I don't know this part of the library but my guess is that this is worth PRing. Does that instance give you the ones you originally wanted (on $\R$, $\mathbb{C}$?). Do you have push access rights for non-master branches on GitHub?

[Marmare314]

Yes it gives at least ℝ, ℝ≥0, ℝ≥0∞ and ℂ. Only EReal is not an instance of Div.
No I don't (my username should be the same as here). Is the process of creating a PR similar to other repositories except that the PR's should be created from a non-master branch?

[Ruben Van de Velde]

More importantly, PRs need to be created from a branch within the main repository rather than a fork

[Kevin Buzzard]

@maintainers can github user marmare314 have push access to non-master mathlib branches for a short PR adding this instance?

[Kevin Buzzard]

Re Ereal: IIRC it was me who made EReal back in the mathlib3 days, and I was very hesitant to put any kind of algebraic structure on it beyond unary Neg because I didn't know what to do with all the infinities, but other people did add these structures (for example it now seems to be a Monoid). But it wouldn't surprise me if it's possible to put an inv on EReal (possibly not involutive) and then make EReal.measurableDiv\2 directly, if you really want it.

[Sébastien Gouëzel]

The inv would have to be really bad, though, as it can't even be involutive: of course the inverse of both infinities should be zero, but then what choice do you make for the inverse of zero?

[Kevin Buzzard]

In my opinion everything other than the Neg is "really bad" on this type, but that doesn't seem to have stopped people defining + and * where it is just as easy to raise objections.

[Kevin Buzzard]

In fact I find it miraculous that addition and multiplication are associative. We can make inverse involutive by just defining $x^{-1}$ to be $x$ for $x\in\{0,\pm\infty\}$ for example, this is no worse than the other atrocities which are happening on this type (at least that's what it feels like to me -- maybe you have some more conceptual way of thinking about it which explains what's happening here).

[Ruben Van de Velde]

Clearly we should extend it with a negative zero

[Marmare314]

But isn't it quite common to work with functions with codomain EReal? Normally you just have to be careful not to accidentally write inf - inf or similar things. This is probably not very convenient in lean.

[Kevin Buzzard]

The philosophy in Lean is to allow users to write junk like $\infty-\infty$ but not to guarantee that the answer is anything sensible. For example we allow $1/0$ as reals, and it's assigned some junk value like 37 (it's not 37 but I wish it were) and then the point is that there are no theorems about a / b when b = 0 so if you ever divide by 0 you're stuck.

[Kevin Buzzard]

I think that if you're doing signed measures then EReal is the perfect place to be, but I've not had enough experience with measure theory in the library to know the ins and outs of what's happening with this type in practice. My guess is that the people who do work with measure theory thought carefully about junk values for + and *, and it looks like they didn't need / for some reason.

[Marmare314]

I am currently just confused about the implications of using EReal if the edge cases are just defined to somehow work. It's of course fine, since as with division by zero, there are no lemmas allowing wrong conclusions. But somehow it feels worse for that type.
I actually don't really need division on EReal. What I am currently doing is just restating and proving some theorems of the first chapter of Rudin in order to get to know a bit of the library. There quite a few theorems are stated with codomain EReal and now I'm not really sure if it's the best thing to do that in lean too.

[Marmare314]

On that note: Is there a similar statement to iSup_apply for liminf?

[Kevin Buzzard]

The best way to ask questions like this is to write a #mwe with a sorry.

[Marmare314]

Oh of course:

import Mathlib
example [MeasurableSpace X] {f : ℕ → X → EReal} (f_meas : ∀ n, Measurable (f n)) : Measurable (Filter.limsup f atTop) := by
  convert measurable_limsup f_meas
  sorry

Also I couldn't find any lemmas for this either

import Mathlib
example [MeasurableSpace X] {f : ℕ → X → EReal} (f_meas : ∀ n, Measurable (f n)) : - Filter.limsup f atTop = Filter.limsup (-f) atTop := by
  sorry

[Sébastien Gouëzel]

For measure theory, you're probably better off considering functions with range ENNReal. As a historical note, measure theory in Isabelle started using EReal, and then they switched to ENNReal as it is so much better behaved. And Mathlib has been strongly inspired by the Isabelle design.

[Kim Morrison]

Kevin Buzzard said:

maintainers can github user marmare314 have push access to non-master mathlib branches for a short PR adding this instance?

@Marmare314, please check you github invitations!

[Kim Morrison]

Tomas Skrivan said:

With fun_prop the proof would be simp only [div_eq_mul_inv]; fun_prop.

fun_prop can even infer measurability from continuity, see this example

However, it is not merged to the master branch yet. Scott Morrison do you know if anyone else is planning on reviewing it or can we merge it?

Merged!

[llllvvuu]

I am finding this already exists:

import Mathlib.MeasureTheory.Constructions.BorelSpace.Complex

instance (G : Type*) [DivInvMonoid G] [MeasurableSpace G] [MeasurableInv G] [MeasurableMul₂ G] :
    MeasurableDiv₂ G := inferInstance
instance : MeasurableDiv₂ ℝ := inferInstance
instance : MeasurableDiv₂ ℂ := inferInstance

If you are not seeing this, maybe you are missing an import. Or, something that happened to me just recently is that Lean timed out while looking for the instance. In that case putting the first inferInstance explicitly helps.

[llllvvuu]

Here is a #mwe for the timeout:

import Mathlib

instance : MeasurableDiv₂ ℂ := inferInstance

Note that

import Mathlib.MeasureTheory.Constructions.BorelSpace.Complex

instance : MeasurableDiv₂ ℂ := inferInstance

does not time out. So, it must have something to do with there being too many instances in scope.

[Marmare314]

llllvvuu said:

I am finding this already exists:

It seems like it does. Is there any way to see which instance is inferred by lean?

[Eric Wieser]

You can use #synth

[Marmare314]

Scott Morrison said:

Marmare314, please check you github invitations!

Thanks!

[Marmare314]

Eric Wieser said:

You can use #synth

Very good to know, thanks!

measurableDiv₂_of_mul_inv seems to be defined in the same place as most other instances, but with priority 100. I'm not really sure what that means.