norm of abs

Stream: new members

[Christopher Hoskin]

The first lemma is easily proved. The second should follow trivially, but Lean will not accept my proof - it says

rewrite tactic failed, did not find instance of the pattern in the target expression
  max b (-b)

what am I doing wrong please?

import analysis.normed_space.ordered

universe v

variables {β : Type v} [linear_ordered_add_comm_group β]  [normed_group β]

lemma norm_max_eq_norm (b : β) : ∥max b (-b)∥ = ∥b∥ :=
begin
  cases le_total  b (-b)  with bn bp,
  { rw max_eq_right bn, simp, },
  { rw max_eq_left bp, }
end

lemma norm_abs_eq_norm (b : β) : ∥abs b ∥ = ∥b∥ :=
begin
  unfold abs,
  cases le_total  b (-b)  with bn bp,
  { rw max_eq_right bn, simp, },
  { rw max_eq_left bp, }
end

Thanks,

Christopher

[Kevin Buzzard]

lemma norm_abs_eq_norm (b : β) : ∥abs b ∥ = ∥b∥ :=
begin
  unfold abs,
  cases le_total  b (-b)  with bn bp,
  { convert norm_max_eq_norm b,
    /-
    linear_ordered_add_comm_group.to_add_comm_group β = normed_group.to_add_comm_group
    -/
    sorry,
  },sorry
end

When you write [linear_ordered_add_comm_group β] Lean puts the structure of a linear ordered additive group on beta; when you write [normed_group β] it puts a totally different structure of a normed additive group on beta. They might have different 0's, different additions etc. The goal after convert is the statement that the two group structures coincide -- the way you have set things up, they don't.

[Kevin Buzzard]

Unfortunately, normed_group is defined in analysis.normed_space.basic and this file does not have the magic words set_option old_structure_cmd true in it, so I do not know how to fix this.

[Christopher Hoskin]

Okay, thanks, that makes sense. So I can add that as an additional hypothesis and it works.

lemma norm_abs_eq_norm (h: linear_ordered_add_comm_group.to_add_comm_group β = normed_group.to_add_comm_group) (b : β) : ∥abs b ∥ = ∥b∥ :=
begin
  unfold abs,
  convert norm_max_eq_norm b,
end

[Kevin Buzzard]

You can, but this solution will not scale. Type class inference expects there to be only one (at most) structure of add_comm_group on a type, up to definitional equality. Your solution will hence be a nightmare to use. What is even more worrying is that adding set_option old_structure_cmd true to analysis.normed_space.basic makes Lean segfault, a rather rare occurrence nowadays.

[Christopher Hoskin]

It works in the case that β is ℝ.

import analysis.normed_space.ordered

universe v

variables {β : Type v} [linear_ordered_add_comm_group β]  [normed_group β]

lemma norm_max_eq_norm (b : β ) : ∥max b (-b)∥ = ∥b∥ :=
begin
  cases le_total  b (-b)  with bn bp,
  { rw max_eq_right bn, simp, },
  { rw max_eq_left bp, }
end

lemma norm_abs_eq_norm (b : ℝ) : ∥abs b ∥ = ∥b∥ :=
begin
  unfold abs,
  apply norm_max_eq_norm b,
end

[Alex J. Best]

What sort of mathematical object are you trying to model by assuming a normed group whose order is linear?

[Kevin Buzzard]

That's because the reals have been given a compatible normed group and linear ordered group structure.

[Kevin Buzzard]

Alex that's a fair question, but another fair question is whether it is possible to make such a structure in mathlib.

[Christopher Hoskin]

@Alex J. Best - I've proved that the continuous bounded real-valued functions on a topological space form a lattice under the natural ordering - I was just trying to see if the result still held if I replaced ℝ with a more abstract structure.

[Kevin Buzzard]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/old.20structure.20command.20segfault/near/226068687 . I might well be missing an obvious way to do this.

[Alex J. Best]

You can define the class you want like this :

import analysis.normed_space.ordered

class linear_normed_group (α : Type*) extends linear_order α, normed_group α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)

instance a {α : Type*} [h : linear_normed_group α] : linear_ordered_add_comm_group α :=
{..h}

[Kevin Buzzard]

This solution doesn't scale, but I agree that right now it seems like the best way to do it.

[Alex J. Best]

Why doesn't it scale?

[Kevin Buzzard]

I mean, you had to add a random axiom when we have a perfectly good class (linear_ordered_add_comm_group) which already contained that axiom. What if it had been a normed locally ringed add_comm_topos or something?

[Alex J. Best]

But I've made an instance of the original class so, while there was a little bit of copy pasting to set this up it should be now invisible to the user that it was set up this way instead of the old structure command way.

[Alex J. Best]

I think Leo's suggestion was that if mathlib users want to write automation in lean 4 to not have to do the copy-pasting of the axioms by hand (and therefore not break as much if someone renames one?) that should be doable.

[Kevin Buzzard]

Fair enough, I was just envisaging a situation where you had to add a gazillion axioms but I agree it's just the structure def.

[Alex J. Best]

@Christopher Hoskin if you add the lines

class linear_normed_group (α : Type*) extends linear_order α, normed_group α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)

instance a {α : Type*} [h : linear_normed_group α] : linear_ordered_add_comm_group α :=
{..h}

to the top of your file you should be able to replace

variables {β : Type v} [linear_ordered_add_comm_group β]  [normed_group β]

with

variables {β : Type v} [linear_normed_group β]

and hopefully everything should work!

[Christopher Hoskin]

Alex J. Best said:

What sort of mathematical object are you trying to model by assuming a normed group whose order is linear?

@Alex J. Best , @Kevin Buzzard Thanks for your help. Sorry for the delay in replying, but I've been considering this question, and I think the right sort object to model for this problem is a normed lattice ordered group (like a Riesz space, but without real-valued scalar multiplication or completeness of the norm. I've defined a lattice ordered group as follows (c.f. L. Fuchs, "Partially ordered algebraic systems" Chapter V):

class has_abs (α : Type u) := (abs : α → α)

local notation `|`a`|` := has_abs.abs a

class lattice_add_comm_group (α : Type u)
  extends add_comm_group α, lattice α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)

instance lattice_add_comm_group_has_abs [lattice_add_comm_group α] : has_abs (α)  := ⟨λa, a⊔-a⟩

I made has_abs a class, as there are other structures which have a notion of absolute value (e.g. certain GM-spaces and GL-spaces).

I've then proved a number of results including

lemma abs_abs_eq_abs (a : α) : |a| = | |a| | := sorry

(proof omitted for brevity - the absence of scalar multiplication by 1/2 introduces some subtleties!)

Then for the normed lattice ordered group,

class normed_lattice_add_comm_group (α : Type u)
  extends normed_group α, lattice α, has_abs α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
(solid : ∀ a b : α, |a| ≤ |b| → ∥a∥ ≤ ∥b∥)
instance a {α : Type*} [h : normed_lattice_add_comm_group α] : lattice_add_comm_group α :=
{..h}

Mostly, this seems to do what I want:

variables {β : Type u} [normed_lattice_add_comm_group β]

variables (d : β)

lemma test : |d| = d⊔(-d) :=
begin
  unfold has_abs.abs,
end

lemma test2 : |d| =| |d| |   :=
begin
  apply abs_abs_eq_abs,
end

However, it goes a bit wrong when I try to prove:

lemma max_abs_eq_norm (b : β) : ∥| b |∥ = ∥b∥ :=
begin
  rw le_antisymm_iff,
  split,
  {
    apply normed_lattice_add_comm_group.solid,
    rw ← abs_abs_eq_abs b,
  },
  {
    apply normed_lattice_add_comm_group.solid,
    rw ← abs_abs_eq_abs b,
  }
end

Perhaps I am missing a coercion?

Christopher

[Kevin Buzzard]

I can't manage to put your posts together into one file -- I am getting errors with abses. Can you just post one #mwe ? Just to be clear -- I'm saying that I can't set things up so I can see the problem you are seeing. Thanks. PS your proof of test should probably be refl.

[Christopher Hoskin]

Kevin Buzzard said:

I can't manage to put your posts together into one file -- I am getting errors with abses. Can you just post one #mwe ? Just to be clear -- I'm saying that I can't set things up so I can see the problem you are seeing. Thanks. PS your proof of test should probably be refl.

Thanks for your help. Here is a mwe:

import algebra.ordered_group
import analysis.normed_space.basic

universe u
variable {α : Type u}

-- Notation class for absolute value of an element
class has_abs (α : Type u) := (abs : α → α)

-- Write |a| for the absolute value of a
local notation `|`a`|` := has_abs.abs a

-- Define a lattice ordered group
class lattice_add_comm_group (α : Type u)
  extends add_comm_group α, lattice α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)

-- Define the absolute value of an element of a lattice ordered group
instance lattice_add_comm_group.to_has_abs [lattice_add_comm_group α] : has_abs (α)  := ⟨λa, a⊔-a⟩

-- Every lattice additive commutative group is also an ordered additive commutative group
instance lattice_add_comm_group.to_ordered_add_comm_group (α : Type u)
  [s : lattice_add_comm_group α] : ordered_add_comm_group α :=
{ add := s.add, ..s }

-- Absolute value is idempotent
lemma abs_idempotent [lattice_add_comm_group α] (a : α) : | |a| | = |a| := sorry

-- Define a normed lattice ordered group
class normed_lattice_add_comm_group (α : Type u)
  extends normed_group α, lattice α, has_abs α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
(solid : ∀ a b : α, |a| ≤ |b| → ∥a∥ ≤ ∥b∥)

-- Every normed lattice ordered group is a lattice ordered group
instance a {α : Type*} [h : normed_lattice_add_comm_group α] : lattice_add_comm_group α :=
{..h}

-- Let β be a normed lattice ordered group
variables {β : Type u} [normed_lattice_add_comm_group β]

-- Lean can infer the definition of the absolute value
lemma test (b : β) : |b| = b⊔(-b) :=
begin
  refl,
end

-- Lean knows that abs_idempotent holds for normed lattice ordered group
lemma test2 (d : β) : | |d| | = |d| :=
begin
  apply abs_idempotent,
end

/-
But `rw` fails here with:

rewrite tactic failed, did not find instance of the pattern in the target expression
  | |b| |
state:
β : Type u,
_inst_1 : normed_lattice_add_comm_group β,
b : β
⊢ | |b| | ≤ |b|

Or, with set_option pp.all true

rewrite tactic failed, did not find instance of the pattern in the target expression
  @has_abs.abs.{u} β (@lattice_add_comm_group.to_has_abs.{u} β (@a.{u} β _inst_1))
    (@has_abs.abs.{u} β (@lattice_add_comm_group.to_has_abs.{u} β (@a.{u} β _inst_1)) b)
state:
β : Type u,
_inst_1 : normed_lattice_add_comm_group.{u} β,
b : β
⊢ @has_le.le.{u} β
    (@preorder.to_has_le.{u} β
       (@partial_order.to_preorder.{u} β
          (@semilattice_inf.to_partial_order.{u} β
             (@lattice.to_semilattice_inf.{u} β (@normed_lattice_add_comm_group.to_lattice.{u} β _inst_1)))))
    (@has_abs.abs.{u} β (@normed_lattice_add_comm_group.to_has_abs.{u} β _inst_1)
       (@has_abs.abs.{u} β (@lattice_add_comm_group.to_has_abs.{u} β (@a.{u} β _inst_1)) b))
    (@has_abs.abs.{u} β (@normed_lattice_add_comm_group.to_has_abs.{u} β _inst_1) b)
-/

lemma norm_abs_eq_norm (b : β) : ∥| b |∥ = ∥b∥ :=
begin
  rw le_antisymm_iff,
  split,
  {
    apply normed_lattice_add_comm_group.solid,
    rw abs_idempotent b,
    sorry
  },
  {
    apply normed_lattice_add_comm_group.solid,
    rw abs_idempotent b,
  }
end

Not sure if it is better to introduce the absolute value as I have done here, or to have lattice_add_comm_group extend has_abs and introduce it that way?

Christopher

[Eric Wieser]

Changing normed_lattice_add_comm_group to extend lattice_add_comm_group may help

[Eric Wieser]

As might set_option old_structure_cmd true

[Kevin Buzzard]

    apply normed_lattice_add_comm_group.solid,
    apply le_of_eq,
    convert abs_idempotent b,
    -- ⊢ normed_lattice_add_comm_group.to_has_abs = lattice_add_comm_group.to_has_abs

[Kevin Buzzard]

Your normed_lattice_add_comm_group takes something with a normed group structure, a lattice structure, and an abs structure which might be completely unrelated to these other two structures, puts a second abs on it coming from the normed group and lattice structure, and then is complaining (correctly) that these two abs structures are unrelated to each other.

[Christopher Hoskin]

Yes, that makes sense - I was thrown off guard by the test and test2 lemmas holding. I guess they work because Lean can cast everything to lattice_add_comm_group whereas in the norm_abs_eq_norm lemma the solid axiom is stated before Lean knows that normed_lattice_add_comm_group is an instance of lattice_add_comm_group?

One way of working around this appears to be the following:

-- Define a normed lattice ordered group
class normed_lattice_add_comm_group (α : Type u)
  extends normed_group α, lattice α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
(solid' : ∀ a b : α, a⊔-a ≤ b⊔-b → ∥a∥ ≤ ∥b∥)

-- Every normed lattice ordered group is a lattice ordered group
instance a {α : Type*} [h : normed_lattice_add_comm_group α] : lattice_add_comm_group α :=
{..h}

lemma normed_lattice_add_comm_group.solid [normed_lattice_add_comm_group α] : ∀ a b : α, |a| ≤ |b| → ∥a∥ ≤ ∥b∥ :=
  normed_lattice_add_comm_group.solid'

Unless I'm misunderstanding, I think @Eric Wieser 's suggestion will get us back to my original problem of having two separate group structures defined with no relationship between them?

I'm not yet sufficiently versed in classes to know if my solution is a sensible way of setting things up, but I can proceed with this approach and see how it goes, unless someone wants to make an alternative suggestion?

Thanks again for your time,

Christopher

[Eric Wieser]

you want something like

class normed_lattice_add_comm_group (α : Type u)
  extends normed_group α, lattice_add_comm_group α :=
(solid' : ∀ a b : α, a⊔-a ≤ b⊔-b → ∥a∥ ≤ ∥b∥)

[Kevin Buzzard]

The test examples work because Lean is choosing a random abs and happens to get the right one. If there are two instances of a class defined on a type then things get very unpredictable, I don't have much experience in knowing which one is used in various cases because if you have two instances of a class on a type then that's what needs to be fixed rather than persuading Lean to use one over the other. You have run into a genuine issue here and our current Lean 3 workaround isn't robust and is furthermore not going to work in Lean 4, so at some point somebody will write some machinery which makes all of this easier and you'll be able to do what you were doing initially, but unfortunately we're not there yet. I agree with Alex that this workaround where you extend disjoint fields and then add in the extra fields which you can't get because of clashes is right now the best way to proceed. The other approach would be to make normed_group an old structure but to be quite frank the Lean 4 porting people might tell us at some point to remove all old structure command shenannigans so I'm loathe to put any more in right now.