Dense ordered ring has positive elements < 1/n

Stream: Is there code for X?

[Violeta Hernández]

I want to show that a densely ordered ring has elements less than 1/n for every positive natural. Of course since this is a ring, I have to state this as n * x < 1. In other words:

import Mathlib

example {S : Type*} [LinearOrder S] [Ring S] [IsOrderedRing S] [DenselyOrdered S] (n : ℕ) :
    ∃ q : S, 0 < q ∧ n * q < 1 := sorry

Do we have anything like this?

[Violeta Hernández]

Here's a proof sketch for this. We can first prove the existence of a positive element with 2 * q ≤ 1. For this we just take an arbitrary element x between 0 and 1, then either x or 1 - x have this property. Then, some large enough power of q will have the desired property.

[Violeta Hernández]

(i can finish the proof but I want to make sure we don't have something like this or implying this more easily!)

[Yaël Dillies]

I had a suspicion you could do with much less, and indeed:

import Mathlib.Algebra.Order.Monoid.Defs
import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
import Mathlib.Algebra.Order.Monoid.Unbundled.Pow

variable {M : Type*} [LinearOrder M] [AddCommMonoid M] [ExistsAddOfLE M]
  [IsOrderedCancelAddMonoid M] [DenselyOrdered M] {x : M}

private lemma aux (hx : 0 < x) : ∃ y : M, 0 < y ∧ 2 • y ≤ x := by
  obtain ⟨y, hy, hyx⟩ := exists_between hx
  obtain hyx | hxy := le_total (2 • y) x
  · exact ⟨y, hy, hyx⟩
  obtain ⟨z, hz, rfl⟩ := exists_pos_add_of_lt' hyx
  exact ⟨z, hz, by simpa [two_nsmul] using hxy⟩

lemma exists_nsmul_lt_of_pos (hx : 0 < x) : ∀ n : ℕ, ∃ y : M, 0 < y ∧ n • y < x
  | 0 => ⟨x, by simpa⟩
  | 1 => by simpa using exists_between hx
  | n + 2 => by
    obtain ⟨y, hy, hyx⟩ := exists_nsmul_lt_of_pos hx (n + 1)
    obtain ⟨z, hz, hzy⟩ := aux hy
    refine ⟨z, hz, ?_⟩
    calc
          (n + 2) • z
      _ ≤ (2 * (n + 1)) • z := nsmul_left_monotone hz.le (by omega)
      _ = (n + 1) • 2 • z := by simp [← mul_nsmul]
      _ ≤ (n + 1) • y := by gcongr
      _ < x := hyx

[Violeta Hernández]

Oh wow! I'm surprised that this doesn't even require anything about rings.

[Yaël Dillies]

The trick is iterate your first observation instead of picking a power

[Violeta Hernández]

Mind if I turn this into a PR?

[Yaël Dillies]

Go for it!

[Violeta Hernández]

hmm... I think the dual result

theorem exists_nsmul_gt_of_neg (hx : x < 0) (n : ℕ) : ∃ y : R, y < 0 ∧ x < n • y :=
  sorry

might unfortunately require a ring, since there isn't a dual of docs#ExistsAddOfLE.

[Yaël Dillies]

Of course if you're in a group, then you can dualise everything by negation

[Violeta Hernández]

Oh you're right! Groups should work for this too

[Violeta Hernández]

And indeed they do

[Yaël Dillies]

I don't think the "cancellative add monoid with ExistsAddOfGE" case is interesting enough to warrant the introduction of ExistsAddOfGE, so probably groups it is