lub property

Stream: new members

[Callum Cassidy-Nolan]

Hello, I'm working through the following proof:

import data.real.basic
import field_theory.ratfunc

theorem baby_rudin_c1_p20_a
  (x y : ℝ)
  (h₀ : 0 < x) :
  ∃ n : ℕ, 0 < n ∧ y < n * x :=
begin
  set S : set ℝ := { v : ℝ | ∃ n : ℕ, 0 < n ∧ v = n * x} with hS,
  by_contra h,
  rw not_exists at h,
end

My goal now is to use the fact that R has the least upperbound property so then S being a subset of R that is non-empty and bounded above (by y) we must get some least upperbound a, and I'll use that to get a contradiction.

Can I get a tip as to what the name of these upperbound properties would be called in mathlib?

[Ruben Van de Velde]

"lub" is probably the right abbreviation to search for

[Ruben Van de Velde]

Maybe also bdd_above?

[Callum Cassidy-Nolan]

Taking a look

[Yaël Dillies]

docs#is_lub

[Yaël Dillies]

It goes along docs#is_least and docs#bdd_above

[Callum Cassidy-Nolan]

I want to say that there exists a lub for S as it's a non-empty bounded above subset of R, any hint for that theorem?

[Callum Cassidy-Nolan]

this one? docs#exists_lub_Iio

[Kyle Miller]

docs#Sup is the least upper bound, and facts about the version for real numbers are near docs#real.Sup_def. See for example docs#real.is_lub_Sup

import data.real.basic
import field_theory.ratfunc

theorem baby_rudin_c1_p20_a
  (x y : ℝ)
  (h₀ : 0 < x) :
  ∃ n : ℕ, 0 < n ∧ y < n * x :=
begin
  set S : set ℝ := { v : ℝ | ∃ n : ℕ, 0 < n ∧ v = n * x} with hS,
  by_contra h,
  push_neg at h,
  have hSn : S.nonempty,
  { use [x, 1],
    simp [S], },
  have hSb : bdd_above S,
  { use y,
    intros a ha,
    obtain ⟨n, hn, rfl⟩ := ha,
    exact h _ hn, },
  have hl := real.is_lub_Sup S hSn hSb,
  -- hl : is_lub S (Sup S)

end

[Kyle Miller]

By the way, you can write that set as { (n * x : ℝ) | (n : ℕ) (h : 0 < n) }. When there are parentheses around the left of the |, it's treated as an expression, and everything to the right of the | is treated as arguments for an existential.

[Kyle Miller]

It's a slightly different definition since it's using exists rather than and for the 0 < n.

[Jireh Loreaux]

How have I never known about this syntax? :face_palm:

[Alex J. Best]

It was only added a couple of years ago in the community edition, so while its been around for a while its not as widely known/used as things in core that are discussed in #tpil etc.

[Callum Cassidy-Nolan]

Kyle Miller said:

docs#Sup is the least upper bound, and facts about the version for real numbers are near docs#real.Sup_def. See for example docs#real.is_lub_Sup

import data.real.basic
import field_theory.ratfunc

theorem baby_rudin_c1_p20_a
  (x y : ℝ)
  (h₀ : 0 < x) :
  ∃ n : ℕ, 0 < n ∧ y < n * x :=
begin
  set S : set ℝ := { v : ℝ | ∃ n : ℕ, 0 < n ∧ v = n * x} with hS,
  by_contra h,
  push_neg at h,
  have hSn : S.nonempty,
  { use [x, 1],
    simp [S], },
  have hSb : bdd_above S,
  { use y,
    intros a ha,
    obtain ⟨n, hn, rfl⟩ := ha,
    exact h _ hn, },
  have hl := real.is_lub_Sup S hSn hSb,
  -- hl : is_lub S (Sup S)

end

This is really useful, I'm trying to imitate this proof:

image.png

So I'm wondering if anyone knows of any theorems in mathlib that would help with

"since alpha - x < alpha, and alpha is the least upper bound we get that alpha - x is not a lower bound, so then there exists a positive integer m so that alpha - x < mx, and then keep going for the contradiction"?

[Yaël Dillies]

docs#exists_lt_of_lt_cSup

[Callum Cassidy-Nolan]

I got the proof down to this:

import data.real.basic
import field_theory.ratfunc

theorem baby_rudin_c1_p20_a
  (x y : ℝ)
  (h₀ : 0 < x) :
  ∃ n : ℕ, 0 < n ∧ y < n * x :=
begin
  set S : set ℝ := { (n * x : ℝ) | (n : ℕ) (h : 0 < n) } with hS,
  by_contra h,
  push_neg at h,
  have hSn : S.nonempty,
  { use [x, 1],
    simp [S], },
  have hSb : bdd_above S,
  { use y,
    intros a ha,
    obtain ⟨n, hn, rfl⟩ := ha,
    exact h _ hn, },
  have hl := real.is_lub_Sup S hSn hSb,
  let α := Sup S,
  have hlt : α - x < Sup S, sorry,
  have h := exists_lt_of_lt_cSup hSn hlt,
  cases h with b hb,
  cases hb with hSk hb,
  obtain ⟨n, hn, rfl⟩ := hSk,
  have hltx : α < (n + 1) * x, sorry,
  have hnin : α ∉ upper_bounds S, sorry,
  -- contradiction using hl and hnin to finish...
end

So there's a few things I'm struggling with to finish that proof, an tips on how I can get this working? (P.S I took a little break from lean so I'm a little rusty rn)

[Ruben Van de Velde]

For the first sorry, I guessed the name of the relevant lemma: docs#sub_lt_self

[Ruben Van de Velde]

And exact hnin hl.1, finishes the proof, since is_lub is deep down α ∈ upper_bounds S ∧ _

[Ruben Van de Velde]

There's probably a better way to spell hl.1, but I couldn't find it just now

[Ruben Van de Velde]

Btw, I'm assuming you're mostly doing this to get used to lub arguments, because there's a direct three-line proof of the lemma as well

[Ruben Van de Velde]

Final one before I head off: guessing lemma names found sub_lt_iff_lt_add and add_one_mul for the second sorry

[Callum Cassidy-Nolan]

I managed to finish the proof:

import data.real.basic
import field_theory.ratfunc

theorem baby_rudin_c1_p20_a
  (x y : ℝ)
  (h₀ : 0 < x) :
  ∃ n : ℕ, 0 < n ∧ y < n * x :=
begin
  set S : set ℝ := { (n * x : ℝ) | (n : ℕ) (h : 0 < n) } with hS,
  by_contra h,
  push_neg at h,
  have hSn : S.nonempty,
  { use [x, 1],
    simp [S], },
  have hSb : bdd_above S,
  { use y,
    intros a ha,
    obtain ⟨n, hn, rfl⟩ := ha,
    exact h _ hn, },
  have hl := real.is_lub_Sup S hSn hSb,
  let α := Sup S,
  have hlt : α - x < Sup S,
  {
    have lt_self := lt_add_of_pos_right (Sup S) h₀,
    exact sub_right_lt_of_lt_add lt_self,
  } ,
  have h := exists_lt_of_lt_cSup hSn hlt,
  cases h with b hb,
  cases hb with hSk hb,
  obtain ⟨n, hn, rfl⟩ := hSk,
  have hltx : α < (n + 1) * x,
  {
    have b := lt_add_of_sub_right_lt hb,
    have hb := add_one_mul (n : ℝ) x,
    rw hb,
    exact b,
  },
  have hin : ((n + 1) : ℝ) * x ∈ S,
  {
    use (n + 1),
    split,
    {
      have x := lt_add_one n,
      exact lt_trans hn x,
    },
    {
      refl,
    }
  },
  have hnin : α ∉ upper_bounds S,
  {
    intro h,
    let hc := not_lt_of_le (h hin),
    exact hc hltx,
  } ,
  exact hnin hl.1,
end

But I had a few questions:

1) How does simp [S], on line 14 finish the sub proof?
2) What does obtain ⟨n, hn, rfl⟩ := ha, on line 18 actually do? Curious about the rfl part
3) Is there anything that could be done to shorten the proof?

[Kevin Buzzard]

For 2) you can read about the rfl Easter egg in my course notes here but I'd be surprised if it's not mentioned in the docstring of the tactic.