## Stream: Is there code for X?

### Topic: positive reals

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

#### Kevin Buzzard (Apr 15 2021 at 06:56):

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

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

#### Damiano Testa (Apr 15 2021 at 06:57):

Let see if using units nnreal makes it easier!

#### Damiano Testa (Apr 15 2021 at 07:08):

Ok, this works:

instance : ordered_comm_group (units ℝ≥0) := by apply_instance


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

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

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


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


#### Damiano Testa (Apr 15 2021 at 07:34):

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

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

#### Johan Commelin (Apr 15 2021 at 07:40):

It's probably just a hole in the API

#### Johan Commelin (Apr 15 2021 at 07:40):

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

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

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

#### Johan Commelin (Apr 15 2021 at 07:46):

But it's not even about div.

#### Johan Commelin (Apr 15 2021 at 07:46):

But there's enough about le and inv.

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