Zulip Chat Archive

Stream: maths

Topic: Use NeZero for measures?

Yury G. Kudryashov (Jul 21 2023 at 12:27):

What do you think about using [NeZero μ] instead of μ ≠ 0 for measures? Then some lemmas like docs#MeasureTheory.Measure.measure_ne_zero can become instances (and Lean will find this instance, e.g., for volume on a topological group).

Sebastien Gouezel (Jul 21 2023 at 12:44):

Don't we already have a standard way to say that a measure is nonzero, with [μ.ae.NeBot]?

Oliver Nash (Jul 21 2023 at 12:51):

So should we replace docs#MeasureTheory.Measure.measure_ne_zero with

instance measure_ne_zero [Nonempty X] : μ.ae.NeBot := ...

and maybe also add:

instance [NeZero μ] : μ.ae.NeBot := by simp [NeZero.ne μ]

?

Sebastien Gouezel (Jul 21 2023 at 12:55):

In fact I think that the current [μ.ae.NeBot] is rather ugly. I'd rather use [NeZero μ] systematically, and instances between [NeZero μ] and [μ.ae.NeBot] (since cycles are not harmful any more, if I understand correctly).

Oliver Nash (Jul 21 2023 at 12:58):

So we should:

  1. change existing uses of μ.ae.NeBot to NeZero μ,
  2. create a (cyclic!) pair of instances between these two,
  3. turns docs#MeasureTheory.Measure.measure_ne_zero into an instance of NeZero μ (as Yury suggests).

Oliver Nash (Jul 21 2023 at 12:58):

Would you like me to do this?

Sebastien Gouezel (Jul 21 2023 at 13:01):

I would be in favor of that, but we should wait for other people's reaction before embarking on this change. @Yury G. Kudryashov, for instance, what do you think?

Kevin Buzzard (Jul 21 2023 at 13:29):

BTW has anyone actually tested this "cycles no longer considered harmful" claim in the wild?

Yaël Dillies (Jul 21 2023 at 13:38):

I myself came last week to the conclusion that we should replace μ.ae.ne_bot with ne_zero μ. This is what I'm doing in !3#18506.

Eric Rodriguez (Jul 21 2023 at 13:42):

I thought !3 was considered harmful?

Yury G. Kudryashov (Jul 21 2023 at 14:12):

@Yaël Dillies doesn't like Lean 4 and !3#18506 is not-too-late.

Kevin Buzzard (Jul 21 2023 at 14:17):

Only because they changed the tag ;-) (but apparently for a valid reason!)

Yury G. Kudryashov (Jul 21 2023 at 14:40):

@Yaël Dillies I don't see ne_zero in !3#18506

Yaël Dillies (Jul 21 2023 at 14:41):

Ah sorry, must be in the Bergelson intersectivity one instead

Yury G. Kudryashov (Jul 21 2023 at 15:10):

Was it PRed?

Yury G. Kudryashov (Jul 21 2023 at 15:11):

@Oliver Nash Why do we need the instance [μ.ae.neBot] : NeZero μ?

Oliver Nash (Jul 21 2023 at 15:13):

It's hard to think of when we would need this (if ever) but if it does no harm, then it's free to add it. Nevertheless, I wouldn't mind leaving it out.

Yury G. Kudryashov (Jul 21 2023 at 15:14):

We have <30 matches to either ae.*NeBot or NeBot.*ae in the library (and some of them are false positives). I can prepare a PR tonight.

Yury G. Kudryashov (Jul 21 2023 at 20:07):

#6048 (should not be merged before the port-complete tag is there)

Last updated: Dec 20 2023 at 11:08 UTC