Monotone rational sequence approaching a real number?

Stream: Is there code for X?

[Weiyi Wang]

Is there a theorem like this? (or a few short ones that can prove it)

import Mathlib.Topology.MetricSpace.Pseudo.Defs

theorem exists_rat_seq_strictMono_tendsto_real (x : ℝ):
∃ (u : ℕ → ℚ), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧
Filter.Tendsto (fun n ↦ (u n: ℝ)) Filter.atTop (nhds x) := by sorry

I asked LLM first, and it provided an idea: use exists_seq_strictMono_tendsto find a real sequence first, and then use exists_rat_btwn to find a rational sequence in between. I can see how that works, but before I set off writing a tedious proof, I want to check if there is an elegant way.

[Yury G. Kudryashov]

AFAICT, we don't have this. Please generalize this lemma to a Dense set and PR it.

[Weiyi Wang]

Got it. I'll try

[Yury G. Kudryashov]

We have the IsLUB version, it should help.

[Yury G. Kudryashov]

Then you can use the Dense version to get the original one.

[Weiyi Wang]

Oof, I went on a journey misguided by LLM and almost got it with an unholy proof > 30 lines.

I did a quick search, but it mathlib doesn't seem to have existing theorems involving both IsLUB and Dense. I can intuitively picture how it works (the LUB of a set is also the LUB of the set intersecting the dense set), but it might take me a while to have a concrete proof, as I am not a math major

[Weiyi Wang]

Something like this...

theorem dense_exists_seq_strictMono_tendsto' {α : Type*} [LinearOrder α] [TopologicalSpace α]
    [DenselyOrdered α] [OrderTopology α] [FirstCountableTopology α] {x y : α}
    {s : Set α} (hs : Dense s) (hy : y < x) :
    ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ Ioo y x ∧ u n ∈ s) ∧ Tendsto u atTop (𝓝 x) := by

  obtain ⟨v, hv_mono, hv_mem, hvx⟩ := exists_seq_strictMono_tendsto' hy

  have hv_mono': ∀ n : ℕ, v n < v (n + 1) := by
    intro n
    apply hv_mono
    simp
  have hu_exist := fun (n : ℕ) ↦ hs.exists_between (hv_mono' n)

  use fun (n : ℕ) ↦ (hu_exist n).choose
  constructor
  · apply strictMono_nat_of_lt_succ
    intro n
    trans v (n + 1)
    · exact ((hu_exist n).choose_spec).right.right
    · exact ((hu_exist (n + 1)).choose_spec).right.left
  · constructor
    · intro n
      obtain ⟨hu_mem_s, ⟨hu_lower, hu_upper⟩⟩ := (hu_exist n).choose_spec
      obtain hv_lower := (hv_mem n).left
      obtain hv_upper := (hv_mem (n + 1)).right
      exact ⟨⟨lt_trans hv_lower hu_lower, lt_trans hu_upper hv_upper⟩, hu_mem_s⟩
    · have hv_le_u : ∀ n : ℕ, v n ≤ (hu_exist n).choose := by
        intro n
        exact le_of_lt (hu_exist n).choose_spec.2.1
      have hu_le_x : ∀ n : ℕ, (hu_exist n).choose ≤ x := by
        intro n
        exact le_of_lt (lt_trans (hu_exist n).choose_spec.2.2 (hv_mem (n + 1)).right)
      apply tendsto_of_tendsto_of_tendsto_of_le_of_le hvx tendsto_const_nhds hv_le_u hu_le_x

[Jireh Loreaux]

Here's the argument Yury mentioned, from which you can deduce the existing result. (You're welcome to PR this to Mathlib)

import Mathlib

open Filter Topology Set

protected lemma Set.Subset.isLUB_congr {α : Type*}
    [TopologicalSpace α] [Preorder α] [ClosedIicTopology α]
    {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) {x : α} :
    IsLUB s x ↔ IsLUB t x :=
  isLUB_congr <| (upperBounds_closure (s := s) ▸ upperBounds_mono_set hts).antisymm <|
   upperBounds_mono_set hst

lemma Dense.isLUB_inter_iff {α : Type*} [TopologicalSpace α]
    [Preorder α] [ClosedIicTopology α]
    {s t : Set α} (hs : Dense s) (ht : IsOpen t) {x : α} :
    IsLUB (t ∩ s) x ↔ IsLUB t x :=
  Set.Subset.isLUB_congr (by simp) <| hs.open_subset_closure_inter ht

lemma Dense.exists_seq_strictMono_tendsto {α : Type*}
    [TopologicalSpace α] [LinearOrder α] [OrderTopology α]
    [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α]
    {s : Set α} (hs : Dense s) (x : α) :
    ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ s := by
  have hs₁ : (Iio x ∩ s).Nonempty := by
    obtain ⟨y, hy⟩ := exists_lt x
    obtain ⟨z, hz, hzx⟩ := hs.exists_between hy
    use z
    aesop
  have hsx₁ : IsLUB (Iio x ∩ s) x := hs.isLUB_inter_iff isOpen_Iio |>.mpr isLUB_Iio
  peel hsx₁.exists_seq_strictMono_tendsto_of_not_mem (by aesop) hs₁ with u _ _ _ _
  aesop

example {α : Type*}
    [TopologicalSpace α] [LinearOrder α] [OrderTopology α]
    [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] (x : α) :
    ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x) := by
  peel dense_univ.exists_seq_strictMono_tendsto x with _ _ _ _
  exact this.1

[Jireh Loreaux]

And here's a shorter version of the argument you described (but we should do what Yury suggested for Mathlib).

[Jireh Loreaux]

import Mathlib

open Filter Topology Set

lemma Dense.exists_seq_strictMono_tendsto {α : Type*}
    [TopologicalSpace α] [LinearOrder α] [OrderTopology α]
    [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α]
    {s : Set α} (hs : Dense s) (x : α) :
    ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ (range u ⊆ s) ∧ Tendsto u atTop (𝓝 x) := by
  obtain ⟨v, h_mono, h_lt, h_tendsto⟩ := _root_.exists_seq_strictMono_tendsto x
  have : ∀ n, ∃ y ∈ s, v n < y ∧ y < v (n + 1) :=
    fun n ↦ hs.exists_between (h_mono n.lt_add_one)
  choose u hu using this
  obtain ⟨hu₁, hu₂, hu₃⟩ := by simpa [forall_and] using hu
  have hu₄ (n : ℕ) : u n < x := (hu₃ n).trans (h_lt (n + 1))
  refine ⟨u, ?mono, hu₄, range_subset_iff.mpr hu₁, ?tendsto⟩
  case mono => exact strictMono_nat_of_lt_succ fun n ↦ (hu₃ n).trans (hu₂ (n + 1))
  case tendsto =>
    exact tendsto_of_tendsto_of_tendsto_of_le_of_le
      h_tendsto tendsto_const_nhds (hu₂ · |>.le) (hu₄ · |>.le)

[Weiyi Wang]

oh thanks! I feel the lemma about IsLUB of intersection should probably be extracted and placed somewhere as well.

[Weiyi Wang]

also TIL peel. Never seen this in guides before

[Jireh Loreaux]

The more generic lemma would be something like (hst : s ⊆ t) (hs : t ⊆ closure s) (x : α) : IsLUB s x ↔ IsLUB t x. which is easily provable with docs#upperBounds_closure and docs#upperBounds_mono_set with docs#isLUB_congr.

[Jireh Loreaux]

I've updated the code above with these generic lemmas.

[Kevin Buzzard]

IIRC Jireh wrote peel :-)

[Jireh Loreaux]

Well, yes, and then Kyle rewrote it better! :laughing:

[Jireh Loreaux]

@Weiyi Wang are you planning to PR the above? If not, I'll get around to it.

[Weiyi Wang]

I did, but I can only do it later today (and possibly can only publish it tomorrow). Feel free to open PR if you feel like it, since you likely can do a better job than me finding homes for these code

[Jireh Loreaux]

no, go for it. I just wanted to make sure it wouldn't slip through the cracks

[Weiyi Wang]

Ok, here it is #23648
(I broke peel when adjusting the proof and didn't figure out how to fix it. Sorry for removing it...)

[Weiyi Wang]

I also got a proof specialized in Rat/Real. It turns out not that trivial because I needed to jump around casting. Maybe I should also PR it later. Would that be placed in Mathlib.Topology.Instances.Rat?

[Weiyi Wang]

Hi @Yury G. Kudryashov, could you review the PR above?

[Yury G. Kudryashov]

I'll try to find time for this tonight

[Weiyi Wang]

Thanks!