seminormed group

Stream: maths

[Riccardo Brasca]

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]

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]

Does it work to say,

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

[Heather Macbeth]

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]

I would hope that Heather's suggestion works.

[Johan Commelin]

You will need set_option old_structure_cmd true for that.

[Riccardo Brasca]

It says

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

[Kevin Buzzard]

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

[Riccardo Brasca]

Ops, I answered before seeing Johan's answer

[Johan Commelin]

But it only works if semi_normed_group is also an old structure

[Kevin Buzzard]

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]

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]

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]

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

[Johan Commelin]

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

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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]

Hmm... not at all the same thing

[Riccardo Brasca]

@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]

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

[Sebastien Gouezel]

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

[Johan Commelin]

Probably that is the best thing to do

[Riccardo Brasca]

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]

No, that's not what Sebastien means

[Johan Commelin]

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

[Riccardo Brasca]

Ah, I see!

[Johan Commelin]

But directly after it, you write

instance [normed_group A] : semi_normed_group A := _

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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

[Johan Commelin]

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]

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

[Riccardo Brasca]

#6746 if someone is insterested

[Riccardo Brasca]

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]

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 }

[Yaël Dillies]

Eh! I just read the blogpost and the first thing I thought is that we have docs#seminorm. Should we link docs#semi_normed_group and seminorm somehow?

[Johan Commelin]

Probably doesn't hurt. There can also be glue with docs#valuation I guess?

[Riccardo Brasca]

Ah, I didn't know that! Was it already there? normed_group uses has_norm, that has no assumption.

[Yaël Dillies]

Yeah, Jean Lo did that back in 2019. To be fair though, this is more of a convex analysis thing.

[Yaël Dillies]

Maybe there's a way to generalize both approaches?

[Yaël Dillies]

Note that I'm adding a lot to analysis.seminorm in #9097

[Yaël Dillies]

I think the main difference is that semi_normed_group is about a group with a fixed seminorm, while seminorm is more to manipulate several seminorms on a given group module.

[Riccardo Brasca]

Ah OK, it's not exactly the same. It surely doesn't hurt to link the two notion, but I think that semi_normed_group will not be used a lot.