Zulip Chat Archive

Stream: Is there code for X?

Topic: positive reals


view this post on Zulip Damiano Testa (Apr 15 2021 at 06:54):

Dear All,

do strictly positive reals appear in mathlib? If so, are they an ordered_comm_group?

I searched a bit and could not find them.

Thanks!

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 06:56):

Maybe units nnreal is the closest we have -- assuming nnreal is a monoid...

view this post on Zulip Damiano Testa (Apr 15 2021 at 06:57):

Hmm, I can try. I was playing with the inequalities that Johan suggested in liquid and there are very few lemmas about divisibility that apply to R>0 since it does not have many instances...

view this post on Zulip Damiano Testa (Apr 15 2021 at 06:57):

Let see if using units nnreal makes it easier!

view this post on Zulip Damiano Testa (Apr 15 2021 at 07:08):

Ok, this works:

instance : ordered_comm_group (units 0) := by apply_instance

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 07:10):

If that's the route you want to go down then probably the next thing to do is to define a constructor which takes in a real and a proof that it's positive, and gives you an element of the units.

view this post on Zulip Damiano Testa (Apr 15 2021 at 07:15):

Since it seems that the lemma that I will use most often is a / b ≤ a / c ↔ c ≤ b, with a b c : nnreal, I will just prove this by breaking up the terms and reducing to the real case. Hopefully, I will not need more lemmas!

view this post on Zulip Damiano Testa (Apr 15 2021 at 07:23):

Not too pretty, but this works:

lemma preal.div_le_div_left {a b c : 0} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) :
  a / b  a / c  c  b :=
begin
  cases a with a ha,
  cases b with b hb,
  cases c with c hc,
  have a00 : 0 < a := a0,
  have b00 : 0 < b := b0,
  have c00 : 0 < c := c0,
  erw [div_le_div_left a00 b00 c00],
  exact iff.rfl,
end

view this post on Zulip Rémy Degenne (Apr 15 2021 at 07:31):

lemma preal.div_le_div_left {a b c : 0} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) :
  a / b  a / c  c  b :=
by rw [nnreal.div_le_iff b0.ne.symm, div_mul_eq_mul_div, nnreal.le_div_iff_mul_le c0.ne.symm,
  mul_le_mul_left a0]

view this post on Zulip Damiano Testa (Apr 15 2021 at 07:34):

Rémy, thank you very much! I had not found the nnreal.div_le_iff + ... lemmas!

view this post on Zulip Johan Commelin (Apr 15 2021 at 07:40):

Damiano Testa said:

Since it seems that the lemma that I will use most often is a / b ≤ a / c ↔ c ≤ b, with a b c : nnreal, I will just prove this by breaking up the terms and reducing to the real case. Hopefully, I will not need more lemmas!

Doesn't this work in any linear_ordered_comm_group_with_zero?

view this post on Zulip Johan Commelin (Apr 15 2021 at 07:40):

It's probably just a hole in the API

view this post on Zulip Johan Commelin (Apr 15 2021 at 07:40):

Almost every lemma that's proven for nnreal should work in that generality

view this post on Zulip Damiano Testa (Apr 15 2021 at 07:42):

I could not find the lemmas with inequalities for linear_ordered_comm_group_with_zero: the ones that I found were either for comm_group or field. I was not able to find the with_zero version.

view this post on Zulip Johan Commelin (Apr 15 2021 at 07:46):

There are some holes in the API. https://github.com/leanprover-community/mathlib/blob/master/src/algebra/linear_ordered_comm_group_with_zero.lean#L158 seems to be the only lemma about "div".

view this post on Zulip Johan Commelin (Apr 15 2021 at 07:46):

But it's not even about div.

view this post on Zulip Johan Commelin (Apr 15 2021 at 07:46):

But there's enough about le and inv.

view this post on Zulip Damiano Testa (Apr 15 2021 at 07:47):

Johan, thanks for the pointer: I will try to work with what is available, before trying to fill in the holes!


Last updated: May 19 2021 at 03:22 UTC