# Zulip Chat Archive

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

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

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

Ops, I answered before seeing Johan's answer

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

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

#### Riccardo Brasca (Mar 17 2021 at 20:01):

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

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