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!

[Wrenna Robson]

Here in 2024, what is the best spelling of the positive reals?

[Jireh Loreaux]

How about ℝ≥0ˣ?

[Jireh Loreaux]

What do you want to do with them?

[Jireh Loreaux]

We might even have some API for them as a pure subtype (i.e., { x : ℝ // 0 < x})

[Jireh Loreaux]

Indeed, we have Mathlib.Algebra.Order.Positive.{Field, Ring}.

[Wrenna Robson]

On reflection, I suspect I am better served by having (r : ℝ≥0∞) and making 0<r a hypothesis

[Yury G. Kudryashov]

Do you want to allow infinity? BTW, we're trying to use r ≠ 0 as an assumption for nonnegative types in Mathlib (not very consistently).

[Terence Tao]

There is also the NeZero class if you want to make instance inference do all the verification of positivity for you (though my understanding is that using other methods such as the positivity tactic is preferred).