Do we need `has_norm`

Stream: maths

[Yury G. Kudryashov]

Is there any example where we can't use has_nnnorm instead?

[Yury G. Kudryashov]

I mean, should we force the norm to be nonnegative by definition?

[Yury G. Kudryashov]

(same question for dist/nndist).

[Mario Carneiro]

we might want norm to have a separate defeq from nnnorm

[Yury G. Kudryashov]

When we don't want defeq norm x = (nnnorm x : real)?

[Mario Carneiro]

because norm x might have a natural expression of its own which just happens to be always nonnegative and is not defeq to coercing that real to a nnreal and then back to a real

[Yury G. Kudryashov]

(note: this came up because some lemmas about is_o assume normed_group just to have a nonnegative norm)

[Mario Carneiro]

For example abs (x - y) : real has this property

[Yury G. Kudryashov]

((⟨x, hx : 0 ≤ x⟩ : nnreal) : real) = x is always defeq

[Mario Carneiro]

Maybe to turn it around then: why is nnnorm a field, when it could just be a definition combining the x and hx from a real-valued norm?

[Yury G. Kudryashov]

E.g., the norm on α → β is defined using finset.sup

[Yury G. Kudryashov]

So, we can have a nice defeq for nnnorm on a pi type (though it seems that we don't have it).

[Yury G. Kudryashov]

AFAIR, has_nnnorm was introduced not long ago.

[Yury G. Kudryashov]

/me is running git log -S has_nnnorm

[Mario Carneiro]

I think it is reasonable to just have one class here which adds both fields

[Yury G. Kudryashov]

@Riccardo Brasca added has_nnnorm in #7986. The commit message says that has_nnnorm is useful in LTE.

[Yury G. Kudryashov]

So, I suggest that we wait for comments from LTE people.

[Mario Carneiro]

unless for some reason you want a norm that isn't nonnegative? Looking at you, field norm

[Yury G. Kudryashov]

But if it also doesn't take values in real

[Yury G. Kudryashov]

(at least not necessarily)

[Riccardo Brasca]

I don't remember exactly why LTE was full of non negative norm, maybe @Johan Commelin can say more.
I just realized we were using it a lot and so it was reasonable to have it in mathlib, where almost everything is done using has_norm.

[Riccardo Brasca]

At the end of the day the two notion are equivalent, and I don't have a strong preference over one or the other, but it would be nice to only have one norm. @Yaël Dillies Is this relevant for the refactor you are doing?

[Yaël Dillies]

Which one? :grinning:

[Johan Commelin]

It took care of plenty of nonneg hypotheses for us. You can just take products, and don't have to prove they stay nonneg, etc...

[Johan Commelin]

We almost never use honest ℝ in LTE. So it was really nice to be able to just stay in the ℝ≥0 realm.

[Yaël Dillies]

Either way shouldn't affect any of my refactors.

[Yaël Dillies]

The question is not to get rid of nnnorm, however, right? It's about making it nonprimitive.

[Yury G. Kudryashov]

I suggested to put norm x = (nnnorm x : real) by definition.

[Patrick Massot]

Johan Commelin said:

We almost never use honest ℝ in LTE. So it was really nice to be able to just stay in the ℝ≥0 realm.

My experience is that I hated ℝ≥0 every single second I used it in LTE, mostly because it's less tactic friendly.

[Kevin Buzzard]

So one fix for this is to make better tactics I guess.