## Stream: maths

### Topic: seminormed group

#### 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,


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.

#### 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

#### Heather Macbeth (Mar 17 2021 at 19:43):

Does it work to say,

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


#### 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₂


#### Johan Commelin (Mar 17 2021 at 19:45):

I would hope that Heather's suggestion works.

#### Johan Commelin (Mar 17 2021 at 19:45):

You will need set_option old_structure_cmd true for that.

#### 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


#### Kevin Buzzard (Mar 17 2021 at 19:46):

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

#### Johan Commelin (Mar 17 2021 at 19:46):

But it only works if semi_normed_group is also an old structure

#### 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?

#### 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 -/
(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,
{ 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 α


#### 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)

#### Johan Commelin (Mar 17 2021 at 19:54):

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

#### Johan Commelin (Mar 17 2021 at 19:54):

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

#### 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∥


#### 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.

#### 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 α


#### Riccardo Brasca (Mar 17 2021 at 19:57):

Hmm... not at all the same thing

#### 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)

#### 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.

#### 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.

#### Johan Commelin (Mar 17 2021 at 20:00):

Probably that is the best thing to do

#### 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)


#### Johan Commelin (Mar 17 2021 at 20:00):

No, that's not what Sebastien means

#### Johan Commelin (Mar 17 2021 at 20:00):

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

Ah, I see!

#### Johan Commelin (Mar 17 2021 at 20:01):

But directly after it, you write

instance [normed_group A] : semi_normed_group A := _


#### 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

#### 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) :=


doesn't work, it says

type mismatch at application
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

#### Johan Commelin (Mar 17 2021 at 21:57):

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

#### 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


#### Riccardo Brasca (Mar 17 2021 at 22:10):

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

#### Riccardo Brasca (Mar 17 2021 at 23:53):

#6746 if someone is insterested

#### 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.

#### 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