Zulip Chat Archive

Stream: maths

Topic: seminormed group


view this post on Zulip Riccardo Brasca (Mar 17 2021 at 19:35):

I recently introduced in mathlib pseudo_emetric_space and pseudo_metric_space, with the basic API (essentially I kept what worked out of the box for metric spaces). The next step we need for the LTE is semi_normed_group and I started working on it. (I know, pseudometric but seminormed... this seems the standard terminology).

The natural definition is

class semi_normed_group (α : Type*) extends has_norm α, add_comm_group α, pseudo_metric_space α :=
(dist_eq :  x y, dist x y = norm (x - y))

Just replace metric_space with pseudo_metric_space in the current definition. But how to define normed_group? One possibility is

class normed_group (α : Type*) extends semi_normed_group α :=
(norm_eq_zero_if :  x : α, x = 0  x = 0)

and then putting an instance of a metric_space on a normed_group. I started with this approach but then I realized I had to modify by hand several construction about normed_group. For example for subgroups we currently have

instance add_subgroup.normed_group {E : Type*} [normed_group E] (s : add_subgroup E) :
  normed_group s :=
{ norm := λx, norm (x : E),
  dist_eq := λx y, dist_eq_norm (x : E) (y : E) }

and it becomes something like

instance add_subgroup.normed_group {E : Type*} [normed_group E] (s : add_subgroup E) :
  normed_group s :=
{ norm_eq_zero_if := λ x h,
  begin
    rw [coe_norm_subgroup, norm_eq_zero] at h,
    exact subtype.eq h
  end,
  ..add_subgroup.semi_normed_group s }

The proof is not hard, but is really different (because we are not proving the same thing...). If I have to do this for the bunch of proof in analysis/normed_space/basic no problem, but I am wondering if this is the good approach.

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 19:37):

I am asking because for pseudo_metric this didn't happen, the definition of a metric space is clearly a pseudometric space such that d(x,y)= 0 → x = y, and this becomes literally the previous definition

view this post on Zulip Heather Macbeth (Mar 17 2021 at 19:43):

Does it work to say,

structure normed_group (α : Type*) extends semi_normed_group α, metric_space α

view this post on Zulip Heather Macbeth (Mar 17 2021 at 19:43):

I ask because this is how linear maps (docs#linear_map) are done, just combining several existing structures with no new fields:

structure linear_map (R : Type u) (M : Type v) (M₂ : Type w)
  [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂]
  extends add_hom M M₂, M [R] M₂

view this post on Zulip Johan Commelin (Mar 17 2021 at 19:45):

I would hope that Heather's suggestion works.

view this post on Zulip Johan Commelin (Mar 17 2021 at 19:45):

You will need set_option old_structure_cmd true for that.

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 19:45):

It says

invalid 'structure' header, field 'to_pseudo_metric_space' from 'metric_space' has already been declared

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 19:46):

that's exactly why you need to put that set_option thing before you try it

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 19:46):

Ops, I answered before seeing Johan's answer

view this post on Zulip Johan Commelin (Mar 17 2021 at 19:46):

But it only works if semi_normed_group is also an old structure

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 19:47):

and some of these things aren't, and my instinctive fix (just make them old structures) is...a bad idea? Or just something we can fix with automation when we all finally move to the new structure command?

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 19:51):

The definition gives no error, but the first result for normed_group is

/-- Construct a normed group from a translation invariant distance -/
def normed_group.of_add_dist [has_norm α] [add_comm_group α] [metric_space α]
  (H1 :  x:α, x = dist x 0)
  (H2 :  x y z : α, dist x y  dist (x + z) (y + z)) : normed_group α :=
{ dist_eq := λ x y, begin
    rw H1, apply le_antisymm,
    { rw [sub_eq_add_neg,  add_right_neg y], apply H2 },
    { have := H2 (x-y) 0 y, rwa [sub_add_cancel, zero_add] at this }
  end }

and Lean says

invalid structure value {...}, expected type is known, but it is not a structure
  normed_group α

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 19:53):

I don't know if this is possible, but I am trying to minimize the amount of code to be rewritten (and no problem if it is quite a lot, I just want to be sure I am doing this in the correct way)

view this post on Zulip Johan Commelin (Mar 17 2021 at 19:54):

@Riccardo Brasca what does #print normed_group look like? Before and after your change.

view this post on Zulip Johan Commelin (Mar 17 2021 at 19:54):

Ideally, it would look the same (up to permutation of the fields)

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 19:55):

In current mathlib:

@[class]
structure normed_group : Type u_5  Type u_5
fields:
normed_group.to_has_norm : Π {α : Type u_5} [c : normed_group α], has_norm α
normed_group.to_add_comm_group : Π {α : Type u_5} [c : normed_group α], add_comm_group α
normed_group.to_metric_space : Π {α : Type u_5} [c : normed_group α], metric_space α
normed_group.dist_eq :  {α : Type u_5} [c : normed_group α] (x y : α), dist x y = x - y

view this post on Zulip Sebastien Gouezel (Mar 17 2021 at 19:57):

You can also keep the current mathlib definition, and register by hand an instance from normed_group to semi_normed_group.

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 19:57):

Using Heather's idea

inductive normed_group : Type u_5  Type u_5
constructors:
normed_group.mk : Π {α : Type u_5} [_to_has_norm : has_norm α] [_to_add_comm_group : add_comm_group α]
[_to_pseudo_metric_space : pseudo_metric_space α],
  ( (x y : α), dist x y = x - y)  ( {x y : α}, dist x y = 0  x = y)  normed_group α

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 19:57):

Hmm... not at all the same thing

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 19:58):

@Sebastien Gouezel is seminormed group, I allow the norm to vanish on a nonzero element (but the algebraic structure is still a group)

view this post on Zulip Sebastien Gouezel (Mar 17 2021 at 19:59):

Yes, so a normed group is in particular a seminormed_group, so there is an instance in this direction.

view this post on Zulip Sebastien Gouezel (Mar 17 2021 at 20:00):

It can be automatic if normed_group is defined by extending semi_normed_group, or registered manually otherwise.

view this post on Zulip Johan Commelin (Mar 17 2021 at 20:00):

Probably that is the best thing to do

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 20:00):

Yes, this what I did at the beginning

class normed_group (α : Type*) extends semi_normed_group α :=
(norm_eq_zero_if :  x : α, x = 0  x = 0)

view this post on Zulip Johan Commelin (Mar 17 2021 at 20:00):

No, that's not what Sebastien means

view this post on Zulip Johan Commelin (Mar 17 2021 at 20:00):

He means that you don't change the definition at all.

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 20:01):

Ah, I see!

view this post on Zulip Johan Commelin (Mar 17 2021 at 20:01):

But directly after it, you write

instance [normed_group A] : semi_normed_group A := _

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 20:05):

OK, I have to see if this really works with all the various result, but it seems what I was looking for

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 21:54):

It seems to work better! But I think I am missing something regarding the product. Currently I have

/-- seminormed group instance on the product of two seminormed groups, using the sup norm. -/
instance prod.semi_normed_group : semi_normed_group (α × β) :=
{ norm := λx, max x.1 x.2,
  dist_eq := assume (x y : α × β),
    show max (dist x.1 y.1) (dist x.2 y.2) = (max (x - y).1 (x - y).2), by simp [dist_eq_norm] }

lemma prod.norm_def (x : α × β) : x = (max x.1 x.2) := rfl

lemma prod.nnnorm_def (x : α × β) : nnnorm x = max (nnnorm x.1) (nnnorm x.2) :=
by { have := x.norm_def, simp only [ coe_nnnorm] at this, exact_mod_cast this }

lemma norm_fst_le (x : α × β) : x.1  x :=
le_max_left _ _

lemma norm_snd_le (x : α × β) : x.2  x :=
le_max_right _ _

lemma norm_prod_le_iff {x : α × β} {r : } :
  x  r  x.1  r  x.2  r :=
max_le_iff

for the product of semi_normed_group and then

/-- normed group instance on the product of two normed groups, using the sup norm. -/
instance prod.normed_group : normed_group (α × β) :=
{ norm := λx, max x.1 x.2,
  dist_eq := assume (x y : α × β),
    show max (dist x.1 y.1) (dist x.2 y.2) = (max (x - y).1 (x - y).2), by simp [dist_eq_norm] }

for the product of normed_group. So for example on the product of two normed group there are now two instances of seminormed group (coming from the normed groups product and from the product of the induced semigroups)... is this a problem?

I tried to compile and I have small but strange errors, for example in analysis/normed_space/add_torsor.lean now

lemma uniform_continuous_vadd : uniform_continuous (λ x : V × P, x.1 +ᵥ x.2) :=
(lipschitz_with.prod_fst.vadd lipschitz_with.prod_snd).uniform_continuous

doesn't work, it says

type mismatch at application
  lipschitz_with.prod_fst.vadd
term
  lipschitz_with.prod_fst
has type
  lipschitz_with 1 prod.fst
but is expected to have type
  lipschitz_with ?m_5 ?m_6

But

lemma uniform_continuous_vadd : uniform_continuous (λ x : V × P, x.1 +ᵥ x.2) :=
((@lipschitz_with.prod_fst V P _ _).vadd lipschitz_with.prod_snd).uniform_continuous

works

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:57):

@Riccardo Brasca if the two instances are defeq, it's not a problem

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:58):

You can check this by

example : @seminormed_group.prod X Y (@normed_group.to_seminormed_group_) etc = @normed_group.to_seminormed_group (X \times Y) _ :=
rfl

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 22:10):

This works... I have to investigate a little what is going on...

view this post on Zulip Riccardo Brasca (Mar 17 2021 at 23:53):

#6746 if someone is insterested

view this post on Zulip Riccardo Brasca (Mar 21 2021 at 22:54):

Does someone have an idea why in #6746 I got some weird problems related to products? In analysis/normed_space/basic I have

/-- seminormed group instance on the product of two seminormed groups, using the sup norm. -/
instance prod.semi_normed_group : semi_normed_group (α × β) :=
{ norm := λx, max x.1 x.2,
  dist_eq := assume (x y : α × β),
    show max (dist x.1 y.1) (dist x.2 y.2) = (max (x - y).1 (x - y).2), by simp [dist_eq_norm] }

and

/-- normed group instance on the product of two normed groups, using the sup norm. -/
instance prod.normed_group : normed_group (α × β) := { ..prod.semi_normed_group }

Everything works in that file, but for example in analysis/calculus/fderiv suddenly

lemma has_strict_fderiv_at_fst : has_strict_fderiv_at prod.fst (fst 𝕜 E F) p :=

doesn't work anymore, while

lemma has_strict_fderiv_at_fst : has_strict_fderiv_at (fst 𝕜 E F) (fst 𝕜 E F) p :=

is OK. This is not a big deal, but while working of the continuation of the PR (introducing semi_normed_group_hom and similar things) I see this weird behavior several times, so I think I did something wrong.

view this post on Zulip Riccardo Brasca (Mar 21 2021 at 22:56):

The definition of semi_normed_group and of normed_group is

/-- A seminormed group is an additive group endowed with a norm for which `dist x y = ∥x - y∥`
defines a pseudometric space structure. -/
class semi_normed_group (α : Type*) extends has_norm α, add_comm_group α, pseudo_metric_space α :=
(dist_eq :  x y, dist x y = norm (x - y))

/-- A normed group is an additive group endowed with a norm for which `dist x y = ∥x - y∥` defines
a metric space structure. -/
class normed_group (α : Type*) extends has_norm α, add_comm_group α, metric_space α :=
(dist_eq :  x y, dist x y = norm (x - y))

/-- A normed group is a seminormed group. -/
@[priority 100] -- see Note [lower instance priority]
instance semi_normed_group_of_normed_group [normed_group α] : semi_normed_group α :=
{ dist_eq := normed_group.dist_eq }

Last updated: May 06 2021 at 19:30 UTC