enorm_zero oddities

Stream: mathlib4

[Oliver Butterley]

Why does enorm_zero fails when using it like in this mwe? It also means that simp doesn't close goals that I think it should easily do.

import Mathlib

variable {X V 𝕜 : Type*} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [T2Space V]

example : ‖(0 : V)‖ₑ = 0 := by
  exact enorm_zero
  -- Fails: typeclass instance problem is stuck, it is often due to metavariables
  -- ENormedAddMonoid ?m.6292

#check enorm_zero
-- enorm_zero.{u_8} {E : Type u_8} [TopologicalSpace E] [ENormedAddMonoid E] : ‖0‖ₑ = 0

example : ‖(0 : V)‖ₑ = 0 := by
  have := ofReal_norm_eq_enorm (0 : V)
  simp_all
  -- This ridiculous approach works.

[Riccardo Brasca]

enorm_zero wants a ENormedAddMonoid, but you only have SeminormedAddCommGroup.

[Kevin Buzzard]

I don't know the first thing about this part of the library but two observations: (1) are you sure you want both SeminormedAddCommGroup V and SeminormedGroup V? They are surely putting two unrelated norms on V with the same notation, so you don't know which one you're getting and (2) isn't the convention that the difference between "norm" and "seminorm" is that a seminorm can have nonzero things with norm zero? (sorry if this is nonsense). If so then enorm_zero isn't strong enough for you.

[Kevin Buzzard]

Have you tried writing an enorm_zero' lemma which eats a seminormed object and proves |0|=0 using your "ridiculous" proof? Note that simp_all? reveals that it's using docs#norm_zero which only needs SeminormedAddGroup.

[Riccardo Brasca]

I agree with the two norms, but docs#enorm_zero is true even for seminormed thing, isn't it? It's the easy direction

[Kevin Buzzard]

Right, maybe enorm_zero can be strengthened, but the thing to do is to try and strengthen it and either succeed and make a PR or fail and understand what's going on :-)

[Kevin Buzzard]

For example maybe ESeminormedAddCommGroups don't exist or something.

[Riccardo Brasca]

Well, we don't have any ESemiblahblah

[Oliver Butterley]

Kevin Buzzard said:

(1) are you sure you want both SeminormedAddCommGroup V and SeminormedGroup V? They are surely putting two unrelated norms on V with the same notation, so you don't know which one you're getting

Absolutely, I've removed [SeminormedGroup V]. It came from something ages ago, I didn't delete it when I should have and I didn't see it when copying here.

[Riccardo Brasca]

So, in the second example you move from the extended norm to a standard norm and then the library works

[Kevin Buzzard]

OK so it sounds like the fix is a huge PR with all the boilerplate for ESeminormedMonoids.

[Kevin Buzzard]

Presumably if you are taking enorms of seminormed objects then this is the class you want?

[Sébastien Gouëzel]

The simple fix is to assume [NormedAddCommGroup V]. Is that enough for your applications?

[Michael Rothgang]

Riccardo Brasca said:

enorm_zero wants a ENormedAddMonoid, but you only have SeminormedAddCommGroup.

A NormedAddGroup is an ENormedAddMonoid --- the "seminormed" part is confusing Lean. (edit: oh, that's basically what Sébastien says)

[Oliver Butterley]

Sébastien Gouëzel said:

The simple fix is to assume [NormedAddCommGroup V]. Is that enough for your applications?

Another fix is to add a lemma stating that ‖0‖ₑ = 0 at the beginning of the document using the proof of the fact following the second example. But this is ugly in every possible way! :scream:

Another option would have been to use ENNReal.ofReal ‖μ‖. This is what we had previously but I recently swapped it for ‖μ‖ₑ when I saw that mathlib had that.

We are using this to define total variation for VectorMeasures as a supremum (which in turn is required for complex RMK which in turn is required for the spectral theorem). It seemed best to define variation as generally as possible, even thought we only want it for complex measures at the moment.

[Kevin Buzzard]

Why are you saying that this is ugly? This just looks like any other API lemma. There are plenty of two-line proofs in mathlib of things which would take 0 lines on the board. Just add it to the library if you want it?

[Sébastien Gouëzel]

Since you are assuming that your space is a [NormedSpace 𝕜 V], there is no added generality in assuming [SeminormedAddCommGroup V] over [NormedAddCommGroup V] (since you have a negation coming from multiplication by -1). That's the reason why in this area of mathlib the standing assumption is [NormedAddCommGroup V].

[Kevin Buzzard]

Aah so in fact the answer is "you're doing it wrong"?

[Sébastien Gouëzel]

I tried to say that more gently, Kevin ! :smile:

[Oliver Butterley]

Kevin Buzzard said:

Aah so in fact the answer is "you're doing it wrong"?

Always, but my speed of doing things wrong means speed of learning the right way.

[Oliver Butterley]

Thanks so much for all the help! I'll change it as Sebastien suggests.

[Oliver Butterley]

In conclusion, I learnt (again) that I should actually read and think mathematically about the assumptions scattered in the file.

After paying attention to the full task at hand reasonable assumptions are [TopologicalSpace V] [ENormedAddCommMonoid V] which makes the detail I was asking about and everything else work. (Although several of the enorm results in mathlib needed to be updated to weaker conditions in PR #25371.)