positive reals

Stream: Is there code for X?

[Damiano Testa]

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]

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

[Damiano Testa]

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]

Let see if using units nnreal makes it easier!

[Damiano Testa]

Ok, this works:

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Johan Commelin]

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]

It's probably just a hole in the API

[Johan Commelin]

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

[Damiano Testa]

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]

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]

But it's not even about div.

[Johan Commelin]

But there's enough about le and inv.

[Damiano Testa]

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