normed_ring vs normed_field

Stream: general

[María Inés de Frutos Fernández]

I expected docs#normed_field to be a docs#normed_ring whose underlying ring is a field. However, normed_field uses the more restrictive multiplicative condition ∀ (a b : α), ∥a * b∥ = ∥a∥ * ∥b∥. What is the reason behind this choice?

[Yaël Dillies]

Note, the difference appears at docs#normed_division_ring

[María Inés de Frutos Fernández]

Yes, I saw that too.

[Kevin Buzzard]

I guess this implies that a normed ring which is a field, isn't necessarily a normed field (for example I think that n(x)=min(|x|_p,1) is a perfectly good normed_ring structure on the p-adic numbers). But I think this is probably OK.

[Eric Rodriguez]

But it isn't a mixin, so you'd need to use is_field

[María Inés de Frutos Fernández]

Related to this, there's nothing in the library about normed modules, right? I only found docs#normed_space, which assumes you're working over a docs#normed_field.

[Yaël Dillies]

I believe this could be weakened on the spot.

[María Inés de Frutos Fernández]

Do you mean that we could add a normed_module class, where we replace normed_field by normed_ring? That should be enough for my purposes.

[Yaël Dillies]

No no no! Eric spent six months removing something similar. I mean that normed_space could be redefined by replacing normed_field with normed_ring.

[María Inés de Frutos Fernández]

Oh, so you're saying that all (or at least part of) the existing lemmas will work in that greater generality, so we can just change the definition?

[Yaël Dillies]

That I don't know. I suspect some of them will. My point is that your normed_module has the same axioms as the current normed_space, so it should be the same class.

[Yaël Dillies]

Else, [normed_field 𝕜] [normed_module 𝕜 E] will have less theorems than[normed_field 𝕜] [normed_space 𝕜 E] even though they are mathematically the same.

[María Inés de Frutos Fernández]

Ah, I see what you mean. I'll try to replace normed_field in the normed_space definition and see what breaks.

[María Inés de Frutos Fernández]

Thanks!

[Riccardo Brasca]

Note that what we call "normed field" is usually called a "valued field", and "normed field" only require the inequality.

[Riccardo Brasca]

There is a discussion about this somewhere

[María Inés de Frutos Fernández]

Yes, that's precisely why I expected the definition of normed_field to be different.

[María Inés de Frutos Fernández]

If I use the [ normed_ring R] (is_field R) approach, I can't use inv, right? I think this will be a problem.

[María Inés de Frutos Fernández]

I think it would be easier to add a new class normed_field' that uses the inequality in the definition.

[María Inés de Frutos Fernández]

Riccardo Brasca said:

Note that what we call "normed field" is usually called a "valued field", and "normed field" only require the inequality.

(I'm not saying that normed_field' would be the right name for this new class; I also know that valued_field is in use, so choosing names here would not be trivial).

[Riccardo Brasca]

You can always use docs#is_field.to_field to get an actual field instance, and use inv. But you will lose some definitional equalities

[María Inés de Frutos Fernández]

Even doing that, I don't see how I could use lemmas about inv. For instance, this is one of the first lemmas in analysis/normed_space/basic. I've replaced normed_field by normed_ring in the definition of normed_space and added an is_field α hypothesis to norm_smul.
With the field instance, Lean doesn't complain anymore about a missing has_inv, but the inv_smul_smul₀ and norm_inv in the proof fail (probably because of what you said about defeqs).

import analysis.normed.normed_field

variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*}

noncomputable theory

section prio
set_option extends_priority 920
class normed_space (α : Type*) (β : Type*) [normed_ring α] [semi_normed_group β]
  extends module α β :=
(norm_smul_le : ∀ (a:α) (b:β), ∥a • b∥ ≤ ∥a∥ * ∥b∥)
end prio

variables [normed_ring α] [semi_normed_group β]

set_option pp.all true
lemma norm_smul [normed_space α β] (hα : is_field α) (s : α) (x : β) : ∥s • x∥ = ∥s∥ * ∥x∥ :=
begin
  haveI : field α := hα.to_field,
  by_cases h : s = 0,
  { simp [h] },
  { refine le_antisymm (normed_space.norm_smul_le s x) _,
     calc ∥s∥ * ∥x∥ = ∥s∥ * ∥s⁻¹ • s • x∥     : by rw [inv_smul_smul₀ h]
               ... ≤ ∥s∥ * (∥s⁻¹∥ * ∥s • x∥) :
      mul_le_mul_of_nonneg_left (normed_space.norm_smul_le _ _) (norm_nonneg _)
               ... = ∥s • x∥                 :
      by { rw [norm_inv, ← mul_assoc, mul_inv_cancel (mt norm_eq_zero.1 h), one_mul] }  }
end

[Eric Wieser]

That ought to work with letI instead of haveI

[Eric Wieser]

But I'm not convinced that building API around is_field is the right way to go

[María Inés de Frutos Fernández]

The last line still fails if I switch to letI.

[Yaël Dillies]

Why would you not turn [normed_ring α] (hα : is_field α) into [normed_field α] (assuming the correct definition)?

[María Inés de Frutos Fernández]

Do you mean the <= definition? I would prefer to do that.

[María Inés de Frutos Fernández]

I was trying the is_field approach because it was suggested above (and would avoid creating this new normed_field' class).

[Yaël Dillies]

Creating normed_field' definitely sounds like the right idea.

[Eric Wieser]

(modulo naming choices)

[María Inés de Frutos Fernández]

Do people have opinions about the name of this class / potentially renaming normed_field?

[Eric Wieser]

The alternative would be to replace normed_field K with [field K] [has_multiplicative_norm K] and have [field K] [has_submultiplicative_norm K] for the <= case

[Yaël Dillies]

I'm happy to see normed_field renamed to valued_field, but then we should probably rename normed_division_ring to valued_ring (or valued_division_ring?) as well.

[María Inés de Frutos Fernández]

The natural choices would be normed_field for the <= definition and valued_field for the existing = one, but docs#valued_field exists already.

[Yaël Dillies]

Does it?

[María Inés de Frutos Fernández]

Oh, maybe it doesn't!

[María Inés de Frutos Fernández]

I think I got confused because there's a valued_field file (topology.algebra.valued_field).

[María Inés de Frutos Fernández]

I'm happy with using normed_field and valued_field then (and valued_division_ring).

[Yaël Dillies]

Watch out for name conflicts indeed because we have weird instance names in the file you mentioned. Eg docs#valued_ring.separated

[María Inés de Frutos Fernández]

Maybe it would make sense to rename that instance? I don't see valued_ring used in any other name.

[María Inés de Frutos Fernández]

I've renamed normed_field to valued_field and normed_division_ring to valued_division_ring in #13239. I also renamed valued_ring.separated to valued.separated.

[Moritz Doll]

Doesn't #13239 make the naming really inconsistent? Some things are called normed_foo (groups, spaces) and some are called valued_foo (rings, fields), even though both version just extend has_norm and some algebraic structure

[Yaël Dillies]

The new naming convention will be normed_ to mean ∥a * b∥ ≤ ∥a∥ * ∥b∥ and valued_ for ∥a * b∥ = ∥a∥ * ∥b∥.

[Eric Wieser]

I assume the idea is to add classes with the old names in a subsequent PR

[María Inés de Frutos Fernández]

Yes, exactly, I plan to add normed_division_ring and normed_field in a future PR.

[Eric Wieser]

Can you add something to the PR description explaining that the motivation for the rename is to free up names for those ideas?

[Eric Wieser]

A PR touching 98 files needs a good description! I assume it was just a find and replace? It's usually a good idea to either state explicitly that's all you did, or point out which parts you had to change by hand

[María Inés de Frutos Fernández]

Yes, it was just find and replace. I'll add a description.

[Jireh Loreaux]

Just to be clear, we're not planning to rename the current normed_space to valued_space because of this, are we?

[Adam Topaz]

I have to say that I disagree with the name valued_field for a field endowed with a multiplicative norm. In my experience, the term valued_field refers to a field endowed with a valuation, and while rank one valuations do indeed give rise to such norms, there are higher rank valuations as well. I would suggest submultiplicative_normed_field for the $\le$ version and normed_field (or multiplicative_normed_field) for the $=$ version.

[Adam Topaz]

Now I know somewhat might refer to the nlab page https://ncatlab.org/nlab/show/normed+field where valued_field is mentioned to be defined by Berkovich, but we should keep in mind that Berkovich's notes only consider rank one valuations (he calls them real valuations) because indeed Berkovich spaces are built out of rank one valuations. The approach of Huber, which is now probably more common, uses higher rank valuations as well.

[Adam Topaz]

Actually, looking at this wiki page, https://en.wikipedia.org/wiki/Berkovich_space , I think the names seminormed_field and normed_field could be appropriate.

[Eric Wieser]

Does the token semi in that suggestion align with its meaning in docs#semi_normed_ring vs docs#normed_ring?

[Eric Wieser]

(or phrased differently, which of these two classes should semi_normed_field extend?)

[María Inés de Frutos Fernández]

@Adam Topaz , it's true that this only refers to valuations in the sense of Berkovich or Bosch-Guntzer-Remmert, but I don't think we can use seminormed_field and normed_field (following their notation, a norm is a seminorm in which norm x = 0 implies x = 0). That's the current mathlib convention too.

[María Inés de Frutos Fernández]

I would definitely keep normed_field for the ∥a * b∥ ≤ ∥a∥ * ∥b∥ case, but I would be open to renaming valued_field to something else.

[María Inés de Frutos Fernández]

Maybe rank_one_valued_field?

[Adam Topaz]

What about submultiplicative_seminormed_ring, multiplicative_seminormed_ring and normed_ring as a mixin, which could then be applied to any (commutative?) ring? I guess my main point is that I think word valued should be reserved for valuations, whereas the word (semi)normed should be reserved for (semi)norms.

[Damiano Testa]

To avoid confusion with semi, a shorter spelling of submultiplicative could be le, as in le_seminormed_ring.

[María Inés de Frutos Fernández]

If the main goal is to avoid valued_field/valued_ring (which I agree could create confusion with general valuations), maybe we could just name these multiplicative_normed_field/multiplicative_normed_ring and keep using (semi)normed for the sub-multiplicative classes.

[Patrick Massot]

Maybe I read too quickly, but I think using semi with a different meaning for fields and vector spaces would be really bad. Also note that for analysis the correct class is nondiscrete_normed_field anyway.

[Kevin Buzzard]

real_valued_field?

[Jireh Loreaux]

Personally, I would prefer to keep normed_field as is, and provide a new class submultiplicative_normed_field (or a different name) for the other version. Mathlib's current naming agrees with the literature in at least one place: Topological Vectors Spaces and Their Applications.

[Adam Topaz]

Note that we do have docs#semi_normed_ring .

[Adam Topaz]

Anyway, personally I would be happy with whatever names are chosen for a (sub)multiplicative (semi)normed fields, as long as the name in mathlib isn't of the form *valued*.

[Jireh Loreaux]

Yes, I know, but I don't think it matters. For fields (or division rings), the natural condition is multiplicativity, not submultiplicativity. An intuitive explanation for this is: these objects have inv and the multiplicativity condition is equivalent to docs#norm_inv, so the norm and the inverse play nice. Do we even have a natural example of a (submultiplicatively) normed division ring for which the norm is not multiplicative? I saw Kevin's example above, but it seemed contrived (although I am not qualified to judge such things).

[Kevin Buzzard]

My "min of two valuations" example was indeed contrived; I don't know if it comes up in practice. I don't remember seeing anything like that in Bosch-Guentzer-Remmert (which I've always taken as the canonical reference in the non Archimedean case).

[Sebastien Gouezel]

What about keeping normed_field (which is the most frequent situation, so it should have the shortest name), and adding something like le_normed_field or le_mul_normed_field or submul_normed_field (avoiding the word semi since in mathlib it is associated to norms that can vanish on nonzero elements)?

[Sebastien Gouezel]

(and adding docstrings explaining all this, of course!)

[Jireh Loreaux]

I'm in favor of that as long as we can come up with at least one "naturally occurring" example of such a thing. Otherwise, why would we bother to create this new type class? @María Inés de Frutos Fernández , do you have such an example from your work?

[Yaël Dillies]

le_normed_field or le_mul_normed_field are bad because they sound like lemma names.

[Scott Morrison]

Sebastien's remaining suggestion, submul_normed_field sounds pretty good to my ear. I think people will naturally read submul as "sub-multiplicative", and "sub-multiplicative normed field" is an easy-to-interpret-correctly name.

[Eric Wieser]

I agree with @Jireh Loreaux though that we should have some motivating examples of things that satisfy only that typeclass before adding it

[María Inés de Frutos Fernández]

For the application I have in mind, I actually care about multiplicatively normed fields. I want to prove that if a field K is complete with respect to a rank 1 valuation, and L/K is an algebraic extension, then there's a unique rank 1 valuation on L extending the valuation on K (so in particular, I can extend the p-adic absolute value on $\mathbb{Q}_p$ to $\overline{\mathbb{Q}}_p$, and then define $\mathbb{C}_p$ as the completion of $\overline{\mathbb{Q}}_p$). The reason I wanted to add this submul_normed_field class is that I am following the proof in Bosch-Guentzer-Remmert, and a couple of the results used in the argument are proven for fields with a norm that's only assumed to be power-multiplicative. However, since it seems that no one is planning to use sub-multiplicatively normed fields, I will just formalize those results assuming the existing normed_field.

[Wrenna Robson]

I was directed to this thread after posting the following message. https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Discrete.20metric.2E/near/281125426

[Wrenna Robson]

At best I'm basically struggling to understand a lot of things about the hierarchy here. At least the names (as I think the above discussion might reflect) seem confusing. But in general I feel quite suspicious of the way the whole thing currently works. I was wondering where things are at in general with this.

[Eric Wieser]

I'm of the opinion that a switch from

-- current
variables [normed_ring R] -- ring
variables [normed_ring R] [normed_group M] [normed_space R M]  -- module
variables [comm_ring R] [ring A] [algebra R A] [normed_ring A] [normed_algebra R A] -- algebra

to

-- proposed
variables [ring R] [normed_ring R]
variables [ring R] [add_comm_group M] [module R M] [normed_ring R] [normed_group M] [normed_space R M]
variables [comm_ring R] [ring A] [algebra R A] [normed_ring R] [normed_ring A] [normed_space R A]

might be reasonable, as it gives us the flexibility to mix and match tight vs loose bounds on the multiplication of the norm, and matches how we currently spell

-- current, topology
variables [ring R] [topological_ring R]
variables [ring R] [add_comm_group M] [module R M] [topological_ring R] [topological_add_group M] [has_continuous_const_smul R M]
variables [comm_ring R] [ring A] [algebra R A] [topological_ring A] [has_continuous_const_smul R A]

Obviously it's much more verbose, but we already pay that cost in the topology library.

This would also free us from having separate normed_ring and normed_comm_ring typeclasses, as well as unifying normed_space and normed_algebra.

[Wrenna Robson]

Hang on, I'm not sure variables [normed_ring R] [normed_group M] [normed_space R M] currently works.

[Wrenna Robson]

normed_space is defined only for normed_field.

[Eric Wieser]

Whoops, fixed

[Wrenna Robson]

I think this is closer to what you want, but variables [ring R] [non_unital_semi_normed_ring R] might be better, as it were. Actually what you want really is an equivalent of [has_continuous_const_smul R] for here.

Could you define [has_semimultiplicative_norm R], which requires only [has_norm R], and is basically a wrapper around ∀ (a b : α), ∥a * b∥ ≤ ∥a∥ * ∥b∥? And then also [has_multiplicative_norm R]. How you handle normed_group R I'm less sure of - what about a wrapper [has_dist_eq_norm_sub R] which depends only on [has_sub R], [has_dist R], and [has_norm R], and then wraps around dist x y = ∥x - y∥? That does miss out the metric space aspect and the differentiation between pseudometric and metrics (also, not sure it should be semi_normed_group - surely pseudo_normed_group?)

We don't seem to have an extension of [has_norm R] [has_zero R] [has_neg R] [has_add R] that is basically "∥0∥ = 0", "∥-a∥ = ∥a∥", "∥a + b∥ ≤ ∥a∥ + ∥b∥". It feels like we probably should? Because such a class - call it [norm_pseudogood R] - would then mean that
[add_comm_group R] [has_norm R] [has_dist R] [norm_pseudogood R] [has_dist_eq_norm_sub R] is exactly our current `[sub_normed_group R]".

[Wrenna Robson]

Also, does the notion of a normed_module not make sense? I liked what you first had - we just can't currently do it!

[Eric Wieser]

Could you define [has_semimultiplicative_norm R] <snip>

That is precisely the meaning that normed_ring has in my -- proposed example above

[Wrenna Robson]

It's confusingly named, then - if you look at has_continuous_const_smul, what's nice about that is that it's only asserting a property of - oh you crossed it out.

[Wrenna Robson]

To pick up norm_pseudogood - it is kinda weird that we don't currently have something like this, an ability to say "this norm basically does all the things you want it to do to make a pseudometric out of it". (Obviously a norm has ∥a∥ = 0 -> a = 0 also.)

[Eric Wieser]

Sorry, what I'm proposing is:

-- `add_comm_group ` moved from `extends` to an argument
class normed_group (A) [add_comm_group A]  extends has_norm E, metric_space E :=
(dist_eq : _)

-- this also works for `comm_ring` and everything inbetween
class normed_ring (A) [non_unital_semiring A] extends normed_group A :=
(norm_mul_le : _)

-- could relax the `division_ring` requirement, but that probably doesn't buy anything
class normed_field (A) [division_ring A] extends normed_ring A :=
(norm_mul_eq : _)

-- doesn't extend `module` any more, and may as well relax to `has_scalar` to make typeclass search easier
class normed_space (R A) [has_scalar R A] [has_norm R] [has_norm A] :=
(norm_smul_le : _)

[Wrenna Robson]

Right :) What I'm saying is that that the approach of topology - which is to separate out the properties of the operations from the structure - seems good.

[Wrenna Robson]

I like your normed_space there - it doesn't extend! But if you think about it, kinda odd that it's then called normed_space. And that isn't the approach your other examples give - because they extend the structure.

[Eric Wieser]

Right, you're arguing that you want to go one stage further and break normed_group into smaller pieces than I have there?

[Wrenna Robson]

Yes.

[Eric Wieser]

And that isn't the approach your other examples give - because they extend the structure.

What do you mean by that?

[Sebastien Gouezel]

I'd like to explain why I think it is important to keep normed_field k instead of a bunch of mixins. The problem with mixins is that they lead to combinatorial explosion when new spaces are built out of them, and then new spaces are built out of these new spaces. So in this kind of situation it is better performancewise to have a single typeclass to use that subsumes everything. And it turns out that many many things are built using normed fields (spaces of continuous linear maps, of analytic maps, of continuous multilinear maps, manifolds, and so on).

[Wrenna Robson]

Oh, no, maybe it is the same, I forgot how extending works.

[Wrenna Robson]

Sebastien Gouezel said:

I'd like to explain why I think it is important to keep normed_field k instead of a bunch of mixins. The problem with mixins is that they lead to combinatorial explosion when new spaces are built out of them, and then new spaces are built out of these new spaces. So in this kind of situation it is better performancewise to have a single typeclass to use that subsumes everything. And it turns out that many many things are built using normed fields (spaces of continuous linear maps, of analytic maps, of continuous multilinear maps, manifolds, and so on).

Once you have the mixins, can you not define normed_field as a specific thing?

[Wrenna Robson]

In the way that, say, linear_ordered_add_comm_monoid is really a specific manifestation of a pile of structure.

[Sebastien Gouezel]

Precisely, docs#linear_ordered_add_comm_monoid does not use mixins, it extends a lot of structures.

[Wrenna Robson]

@Eric Wieser the thing about normed_ring extending normed_group is: what if I have a norm on a ring that is submultiplicative on the multplication, but doesn't interact with the addition at all?

[Eric Wieser]

Wrenna Robson said:

Eric Wieser the thing about normed_ring extending normed_group is: what if I have a norm on a ring that is submultiplicative on the multplication, but doesn't interact with the addition at all?

That doesn't strike me as all that useful - but you could always add a normed_monoid in between

[Wrenna Robson]

Sebastien Gouezel said:

Precisely, docs#linear_ordered_add_comm_monoid does not use mixins, it extends a lot of structures.

Right - I think you make a strong argument for having, ultimately, normed_field` present at the top of the hierarchy.

[Eric Wieser]

Sebastien Gouezel said:

Precisely, docs#linear_ordered_add_comm_monoid does not use mixins, it extends a lot of structures.

So would you argue that the topology library should switch to this model?

[Jireh Loreaux]

Note, we're already running into some issues with timeouts in this normed hierarchy. See the end of this thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2313719.3A.20non-unital.20normed.20comm.20ring

[Sebastien Gouezel]

Can you show us a real-world example where you feel our current hierarchy has shortcomings? In a way, our hierarchy is designed to be able to deal with most interesting examples, but if there is a natural situation where it fails it is an interesting datapoint.

[Wrenna Robson]

I suppose I'll re-bring-up the context I was working in from the other thread (where it felt troublesome in part). So I was doing this yesterday (I am trying to formalise some code-based cryptography theorems about a design). https://gist.github.com/linesthatinterlace/25eb6d69d1264fecca89f904d18b4eff

[Sebastien Gouezel]

Eric Wieser said:

So would you argue that the topology library should switch to this model?

No, mixins are fine to specify additional properties of structures that don't show up too much. But the main players in the hierarchy should really be single typeclasses, not one typeclasses with several mixins.

[Wrenna Robson]

I know we already have the L_0 "norm", of a kind, but it isn't actually a norm - except it is if the underlying field has the discrete norm!

[Eric Wieser]

And it turns out that many many things are built using normed fields (spaces of continuous linear maps, of analytic maps, of continuous multilinear maps, manifolds, and so on).

As part of my refactoring of docs#exp, I've found that many things defined in terms of normed_field etc actually generalize just fine to topological rings; so in these cases norm was never a main player after all

[Wrenna Robson]

(well, it's a seminorm)

[Eric Wieser]

I know we already have the L_0 "norm", of a kind

Do we? docs#pi_Lp.normed_space requires p to be positive at least 1

[Wrenna Robson]

https://leanprover-community.github.io/mathlib_docs/measure_theory/function/lp_space.html

[Wrenna Robson]

albeit that is different, but it's clearly tightly related (though I have no idea if there is linking API).

[Sebastien Gouezel]

I don't see the problem with the Hamming distance: you can locally register a normed group instance with the discrete distance on a finite group, and then take its pi_Lp 1, no? (There's no field involved here).

[Jireh Loreaux]

Wrenna, that just gives a garbage value (0) when p=0

[Sebastien Gouezel]

But you really want to use the L^1 distance for the Hamming distance.

[Jireh Loreaux]

I'm not even sure what you mean by L^0 norm Wrenna.

[Sebastien Gouezel]

Eric Wieser said:

As part of my refactoring of docs#exp, I've found that many things defined in terms of normed_field etc actually generalize just fine to topological rings; so in these cases norm was never a main player after all

If you want to do analysis (use derivatives, for instance), you can't do without the normed field structure.

[Eric Wieser]

Regarding shortcomings in the current structure, it would be nice if lemmas like the following would be possible to state:

-- not allowed, ℕ isn't a field
example {M} [normed_group M] [normed_space ℕ M] (n : ℕ) : ∥n • x∥ ≤ ∥n∥ * ∥x∥ := sorry
-- not allowed, `units R` isn't a field
example {R M} [ring R] [normed_group M] [normed_space R M] : normed_space (units R) M := sorry

I guess this is only a complaint about normed_space not the rest of the heirarchy

[Sebastien Gouezel]

Having normed_space only requiring a normed_semiring instead of a normed_field would definitely make sense to me.

[Eric Wieser]

I'm suggesting the stronger change of not even making it extend module, so that it can be used for norm-preserving group actions too (my second example)

[Jireh Loreaux]

I guess R is supposed to be a ring in that second example?

[Jireh Loreaux]

I guess that would also mean changing the definition slightly, so that its norm_smul and not norm_smul_le, right?

[Yaël Dillies]

Yeah, there's really no reason for normed_space to require normed_field. I found myself assuming normed_field in a bunch of place just because normed_space required me to.

[Wrenna Robson]

Eric Wieser said:

I'm suggesting the stronger change of not even making it extend module, so that it can be used for norm-preserving group actions too (my second example)

I agree with this, and I suppose the rest of my complaint is a feeling that we should try to cut down the hierarchy if we can. Also "semi_normed" stuff is ill-named.

[Wrenna Robson]

Also - surely normed_group should be described so that it extends metric_space and semi_normed_group (which should be pseudo_normed_group.

[Jireh Loreaux]

Disagreed about the "semi_normed". This is common terminology. Although I've seen pseudo-normed too. In LCTVS theory I think seminorm is more common.

[Wrenna Robson]

Isn't seminorm normally about the multiplicativity/submultiplicativity stuff?

[Jireh Loreaux]

No? Reference?

[Wrenna Robson]

Oh, no, I'm probably just wrong. I thought someone said it above.

[Wrenna Robson]

The issue I see is that it is easily confused with semiring, which is a different type of semi (I think?).

[Sebastien Gouezel]

Wrenna Robson said:

Also - surely normed_group should be described so that it extends metric_space and semi_normed_group (which should be pseudo_normed_group.

Essentially, it does, in the sense that a normed_group is automatically a metric_space and a semi_normed_group. Whether this is part of the definition or an instance which is registered later on is just a technical detail of the implementation (made in view of performance constraints), but has no practical importance for the end user.

[Yaël Dillies]

Yeah, semi_normed_whatever comes from seminorm. I believe we could get rid of the underscore to make the connection more obvious.

[Wrenna Robson]

Well, I found it mildly confusing, as an end user - but I take your point.

[Yaël Dillies]

Maybe even seminorm_group could be acceptable, and it would save us three keystrokes.

[Wrenna Robson]

If you redefined normed_space to only need a normed_semiring, would you still keep the submultiplicative property for the latter? Does it all work OK if you do that?

[Wrenna Robson]

technically of course it should be seminorm_add_group.

[Yaël Dillies]

Are seminormed multiplicative groups a thing?

[Wrenna Robson]

but what about seminorm_add_semigroup? What, indeed, of semisubmultivativenormed_semiring

[Wrenna Robson]

Yaël Dillies said:

Are seminormed multiplicative groups a thing?

In fairness I don't... think so - but I could believe in them.

[Jireh Loreaux]

Any generalization of normed_space will require changing norm_smul_le to norm_smul.

[Wrenna Robson]

Right. Which suggests we do want to keep track of the submultiplicative distinction...

[Jireh Loreaux]

I think you are conflating mul and smul.

[Yaël Dillies]

Nothing has ever been submultiplicative though. normed_space is currently submultiplicative but that's because we can directly recover multiplicativity from field.

[Wrenna Robson]

Isn't normed_ring submultiplicative?

[Jireh Loreaux]

Yes, but that's mul, not smul

[Wrenna Robson]

I still am not really sure about the bundling of metric_space into the definition of normed_group. Intuitively I would think of a normed_group as a group with a norm added (on which, yes, a metric is induced - I guess the current definition is to ensure you don't have another dist hanging round).

[Wrenna Robson]

Jireh Loreaux said:

Yes, but that's mul, not smul

Oh - I see, right. Why will that need changing?

[Jireh Loreaux]

See docs#normed_space

[Jireh Loreaux]

It has an le right now, but that's because we can prove equality since we have a field. If we don't have a field (or division ring) we can't prove equality, so we need to assume it.

[Wrenna Robson]

And you need to keep the equality - it's not otherwise a useful notion?

[Jireh Loreaux]

Right. And if you didn't, then you would need yet another type class where you have equality.

[Wrenna Robson]

What did you think to the hamming distance thing I posted above?

[Reid Barton]

I'm not quite convinced of that--do you really need a type class for when you have equality? Seems like that usually only happen over a normed field, in which case you can use a lemma

[Reid Barton]

Is $\mathbb{R}^n$ a "normed module" over $M_{n \times n}(\mathbb{R})$ (with the operator norm)?

[Jireh Loreaux]

Hmm, Reid I think you're right. I retract my claim.

[Eric Wieser]

Remember we only recently removed the equality requirement induced by docs#normed_algebra

[Jireh Loreaux]

Wrenna, can you link the hamming distance thing (I'm on mobile)

[Wrenna Robson]

https://gist.github.com/linesthatinterlace/25eb6d69d1264fecca89f904d18b4eff

[Wrenna Robson]

(It would be cool to link this into computability.language somewhat though as I think it's only defined for fixed sizes anyway I'm not sure that's necessary, and I wanted the module structure.)

[Sebastien Gouezel]

As I said above, I think it's just the L^1 distance on the product for the discrete distance on the factor, so we have already all the needed bits in mathlib (with the current hierarchy).

[Wrenna Robson]

Yes, that was my first conclusion :) - though I still (see my other thread) don't know how to quickly put the discrete distance on things.

[Eric Wieser]

(the thread in question is Discrete metric.)

[Wrenna Robson]

Ah, thanks, sorry.

[Wrenna Robson]

Still, thinking of it in terms of finset cardinality (which is closer to the L0 norm perspective) was quite nice and straightforward. Also, I note that if you are defining the hamming distance on something not equipped with sub, you probably can't use the L1 norm.

[Wrenna Robson]

If I re-wrote it to be about set.card instead, you wouldn't even need the decidable_eq predicate - classically you don't, of course.

[Sebastien Gouezel]

Wrenna Robson said:

Still, thinking of it in terms of finset cardinality (which is closer to the L0 norm perspective) was quite nice and straightforward. Also, I note that if you are defining the hamming distance on something not equipped with sub, you probably can't use the L1 norm.

I am not sure it makes a difference whether there is a sub or not: pi_Lp 1 puts a distance on a finite product of metric spaces, it does not require subtraction as far as I can tell.

[Sebastien Gouezel]

Wrenna Robson said:

Yes, that was my first conclusion :) - though I still (see my other thread) don't know how to quickly put the discrete distance on things.

Indeed, I think you are right and this is missing currently!

[Wrenna Robson]

I think in that thead I put my first attempt at it (this is how I was interacting with the hierarchy). The difficulty was that because everything admits the discrete metric, you have to be, uh, really careful about how you define it.

[Wrenna Robson]

Sebastien Gouezel said:

Wrenna Robson said:

Still, thinking of it in terms of finset cardinality (which is closer to the L0 norm perspective) was quite nice and straightforward. Also, I note that if you are defining the hamming distance on something not equipped with sub, you probably can't use the L1 norm.

I am not sure it makes a difference whether there is a sub or not: pi_Lp 1 puts a distance on a finite product of metric spaces, it does not require subtraction as far as I can tell.

I think you are right, thinking about it. Though I wonder - technically there's no reason you can't have an infinite version of the hamming distance, though it wouldn't be a metric space.

[Wrenna Robson]

But in general the "norm" on f : α -> βthat sends it to # (function.support f) is... well, it's certainly defined. Probably not useful though.

[Wrenna Robson]

(It's kinda weird that you could technically assign the hamming norm to a field extension by thinking of it as a vector space under a particular basis, but that completely, I think, will have little or nothing to do with the field structure.)