monotone limits

Stream: Is there code for X?

[Kalle Kytölä]

To my surprise, I failed to library_search a statement that the limit of an increasing sequence is at least any member of the sequence. I needed that for ennreal-valued sequences, but could not find it even for ℝ-valued sequences. I suspect I am doing something wrong in my search. E.g., the following fails:

import topology.instances.real

open set
open filter
open_locale topological_space

lemma tendsto_ge_of_incr_R (s : ℕ → ℝ) (l : ℝ) (incr : monotone s) (lim : tendsto s at_top (𝓝 l)) :
    ∀ n , s(n) ≤ l := by library_search -- fails

I guess the right generality should cover at least both of the above (I'm guessing {τ : Type*} [linear_order τ] [topological_space τ] [order_topology τ]), and also not just sequences. For sequences I have the following clumsy proof (which covers the ℝ, nnreal, and ennreal that I most care about), but what is the right way? And what should I have done to find it?

import topology.algebra.ordered.basic

open set
open filter
open_locale topological_space

lemma tendsto_ge_of_incr {τ : Type*} [ord : linear_order τ] [topo : topological_space τ] [ord_topo : order_topology τ] (s : ℕ → τ) (l : τ)
  (h_incr : monotone s) (h_lim : tendsto s at_top (𝓝 l)) :
    ∀ n , s(n) ≤ l :=
begin
  intros m₀ ,
  by_contra over_lim ,
  simp at over_lim ,
  set U := Iio (s(m₀)) with hU ,
  have hU_nbhd : U ∈ 𝓝 l := Iio_mem_nhds over_lim ,
  have too_high : ∀ (n : ℕ) , n ≥ m₀ → s(n) ∉ U ,
  { intros n hn ,
    simp ,
    exact h_incr hn , } ,
  have key := filter.tendsto_at_top'.mp h_lim U hU_nbhd ,
  cases key with n₀ hn₀ ,
  set k := max n₀ m₀ with hk ,
  specialize hn₀ k (le_max_left n₀ m₀) ,
  specialize too_high k (le_max_right n₀ m₀) ,
  contradiction ,
end

[Kalle Kytölä]

To continue a bit, my first instinct was in fact to look for the completeness axiom of $\R$ formulated along the lines of "all increasing upper bounded sequences have a limit". This is stronger than I asked for above (for the special case of $\R$). I couldn't find this formulation of the completeness axiom. I suspected the failure might be because of my clumsy phrasing of the hypotheses. Perhaps boundedness in the form ∃ (b : ℝ) , ∀ n , s(n) ≤ b is not the right way, or perhaps one should not state the existence of the limit but instead be explicit about the limit being Sup (range s), or something more clever. Anyway, I could not find it in the docs or even by my favorites library_search, tidy, or simp.

So I guess another question I have is: does the above formulation of the completeness axiom of $\R$ exist?

[Kevin Buzzard]

The completeness axiom is formalised as all non-empty bounded-above subsets have a Sup. I don't know if we have this sequence version. A lot of things which one would regard as standard 1st year UG mathematics are proved quite conceptually in Lean, e.g. you probably won't find directly the assertion that the limit of the sum of two sequences of real numbers is the sum of the limits, this will just follow from some general lemma about continuous operators commuting with limits in some huge generality and then we leave it to the type class inference system to insert the proof that addition is continuous on the reals. I don't know my way around the library or the tricks that are used here, but it looks like you're thinking about things in the right way and this lemma might not be there -- you'll have to wait for an analyst to chime in.

[Eric Wieser]

The completeness axioms you're describing sound like those of docs#conditionally_complete_lattice to me

[Eric Wieser]

For which docs#real.conditionally_complete_linear_order provides the instance

[Kevin Buzzard]

There's a theorem of the form "limit = Sup" for monotone sequences, where "limit" is using the order topology and "Sup" is using the lattice structure.

[Kevin Buzzard]

The question is whether this is missing.

[Kevin Buzzard]

more generally you could have an order-preserving function from a total order to a lattice and the claim is that if the sup of the range of the function exists and is L then the function sends at_top to nhds(L) in the sense of filter.tendsto

[Patrick Massot]

The lemma about monotone sequences converging to their sup is docs#tendsto_at_top_csupr

[Patrick Massot]

I compressed your proof a bit.

@[simp]
lemma filter.not_eventually_false {α : Type*} (f : filter α) [ne_bot f] : ¬ (∀ᶠ x in f, false) :=
λ h, ne_bot.ne' (eventually_false_iff_eq_bot.mp h)

open filter

lemma tendsto_ge_of_incr {τ : Type*} [linear_order τ] [topological_space τ]
  [order_topology τ] {s : ℕ → τ} {l : τ}
  (h_incr : monotone s) (h_lim : tendsto s at_top (𝓝 l)) :
    ∀ n , s n  ≤ l :=
begin
  intros m₀ ,
  by_contra over_lim,
  have yes : ∀ᶠ n in at_top, s n ∈ Iio (s m₀),
    from h_lim (Iio_mem_nhds $ not_le.1 over_lim),
  have no : ∀ᶠ n in at_top, s n ∉ Iio (s m₀),
  { suffices : ∃ a, ∀ n ≥ a, s m₀ ≤ s n, by simpa,
    exact ⟨m₀, λ b hb, h_incr hb⟩ },
  simpa only [and_not_self, not_eventually_false] using yes.and no,
end

[Patrick Massot]

The main point is that filters also allow to abstract away the max n₀ m₀ thing.

[Kalle Kytölä]

Thanks a lot everyone!

Kevin's answer about the generality that could be used instead of sequences (functions on ℕ) sounded good to me. I had no idea what a total order is in Lean though... I tried {σ: Type*} [preorder σ] [is_trichotomous σ (_inst_1.lt)] [ne_bot (@at_top σ _inst_1)]. A modification of Patrick's improved proof works in this generality, although the first of the two simpas broke, and I had to resort again to what I am able to write, which of course compromised Patrick's elegance. Anyway, this works:

import topology.instances.real
import topology.instances.ennreal
import init.algebra.classes

open set
open filter
open_locale topological_space

@[simp]
lemma filter.not_eventually_false {α : Type*} (f : filter α) [ne_bot f] : ¬ (∀ᶠ x in f, false) :=
λ h, ne_bot.ne' (eventually_false_iff_eq_bot.mp h)

open filter

lemma tendsto_ge_of_incr {σ τ : Type*} [preorder σ] [is_trichotomous σ (_inst_1.lt)] [ne_bot (@at_top σ _inst_1)]
  [linear_order τ] [topological_space τ] [order_topology τ]
  {s : σ → τ} {l : τ} (h_incr : monotone s) (h_lim : tendsto s at_top (𝓝 l)) :
    ∀ n , s n ≤ l :=
begin
  intros m₀ ,
  by_contra over_lim,
  have yes : ∀ᶠ n in at_top, s n ∈ Iio (s m₀),
    from h_lim (Iio_mem_nhds $ not_le.1 over_lim),
  have no : ∀ᶠ n in at_top, s n ∉ Iio (s m₀),
  { suffices : ∃ a, ∀ n ≥ a, s m₀ ≤ s n,
    { cases this with a ha ,
      have eq : { n | s m₀ ≤ s n } = { n | s n ∉ Iio (s m₀) }
        := by simp only [mem_Iio, not_lt] ,
      have at_least : Ici a ⊆ { n | s n ∉ Iio (s m₀) } := by rwa ← eq ,
      exact at_top.sets_of_superset (mem_at_top a) at_least , } ,
    exact ⟨m₀, λ b hb, h_incr hb⟩ , },
  simpa only [and_not_self, not_eventually_false] using yes.and no,
end

In this generality both of the two cases I actually cared about do indeed work:

• increasing sequences with values in reals
• increasing sequences with values in ennreals.

That much is good (although of course these did already work with my initial pedestrian formulation, too...).

However, only the first of the two seems to be found by library_search, the other one is not found! (Although it works). Here are the specific cases I tried:

lemma tendsto_ge_of_incr_R' (s : ℕ → ℝ) (l : ℝ) (incr : monotone s) (lim : tendsto s at_top (𝓝 l)) :
    ∀ n , s(n) ≤ l := tendsto_ge_of_incr incr lim
    -- works and is found by `library_search`

lemma tendsto_ge_of_incr_ennreal' (s : ℕ → ennreal) (l : ennreal) (incr : monotone s) (lim : tendsto s at_top (𝓝 l)) :
    ∀ n , s(n) ≤ l := tendsto_ge_of_incr incr lim
    -- works but is not found by `library_search` ?!?

Does anyone understand why the first is found and the second is not?

[Kalle Kytölä]

Kevin Buzzard said:

A lot of things which one would regard as standard 1st year UG mathematics are proved quite conceptually in Lean, ...

Yes! I've noticed, and I (sort of) understand why. For me, what often works in practice is to write the undergrad statement in the cleanest possible form, and then apply library_search :grinning_face_with_smiling_eyes: (or a tidy or a simp). This experimental observation of mine is probably a corollary to what you said in "...and then we leave it to the type class inference system to insert the proof". I have been extremely impressed with how well this method works, btw!

And because this is what I almost always do in Lean, I think the working of library_search in the above two cases is sort of important...

[Kalle Kytölä]

One (or $\approx$ one) more question :grinning_face_with_smiling_eyes:...

My original use-case was in fact about decreasing sequences, but because I did not want to write (decr : @monotone ℕ (order_dual τ) _ _ s) I phrased the question here about increasing sequences.

I am of course able to prove the decreasing analogue by changing a few Iios to Iois and a few ≤s to ≥s. But shouldn't there now be some quick shortcut (using order_dual)? Specifically, what would be a good proof of the following, given the proof we already had above?

lemma tendsto_le_of_decr {σ τ : Type*} [preorder σ] [is_trichotomous σ (_inst_1.lt)] [ne_bot (@at_top σ _inst_1)]
  [linear_order τ] [topological_space τ] [order_topology τ]
  {s : σ → τ} {l : τ} (h_decr : @monotone σ (order_dual τ) _ _ s) (h_lim : tendsto s at_top (𝓝 l)) :
    ∀ n , l ≤ s n  := by sorry

Maybe already writing the decreasingness assumption as @monotone σ (order_dual τ) _ _ s is a bit clumsy... Is there a better way?

[Kalle Kytölä]

Ah, sorry --- I now got the first part of my own question about reducing the decreasing case to the increasing case. I clearly should have had more faith in Kevin's advice to "leave it to the type class inference system to insert the proof".

lemma tendsto_le_of_decr {σ τ : Type*} [preorder σ] [is_trichotomous σ (_inst_1.lt)] [ne_bot (@at_top σ _inst_1)]
  [linear_order τ] [topological_space τ] [order_topology τ]
  {s : σ → τ} {l : τ} (h_decr : @monotone σ (order_dual τ) _ _ s) (h_lim : tendsto s at_top (𝓝 l)) :
    ∀ n , l ≤ s n  :=
begin
  set τ' := order_dual τ with hτ' ,
  exact @tendsto_ge_of_incr σ τ' _ _ _ _ _ _ s l h_decr h_lim ,
end

This still leaves the question of is there a better phrasing of (h_decr : @monotone σ (order_dual τ) _ _ s), though.

[Kalle Kytölä]

I also noticed that the [is_trichotomous σ (_inst_1.lt)] is an unnecessary assumption. The Bourbaki assumption [ne_bot (@at_top σ _inst_1)] for the at_top-filter is enough:

import init.algebra.classes
import topology.algebra.ordered.basic

open set
open filter
open_locale topological_space

@[simp]
lemma filter.not_eventually_false {α : Type*} (f : filter α) [ne_bot f] : ¬ (∀ᶠ x in f, false) :=
λ h, ne_bot.ne' (eventually_false_iff_eq_bot.mp h)

open filter

lemma tendsto_ge_of_incr {σ τ : Type*} [preorder σ] [ne_bot (@at_top σ _inst_1)]
  [linear_order τ] [topological_space τ] [order_topology τ]
  {s : σ → τ} {l : τ} (h_incr : monotone s) (h_lim : tendsto s at_top (𝓝 l)) :
    ∀ n , s n ≤ l :=
begin
  intros m₀ ,
  by_contra over_lim,
  have yes : ∀ᶠ n in at_top, s n ∈ Iio (s m₀),
    from h_lim (Iio_mem_nhds $ not_le.1 over_lim),
  have no : ∀ᶠ n in at_top, s n ∉ Iio (s m₀),
  { suffices : ∃ a, ∀ n ≥ a, s m₀ ≤ s n,
    { cases this with a ha ,
      have eq : { n | s m₀ ≤ s n } = { n | s n ∉ Iio (s m₀) }
        := by simp only [mem_Iio, not_lt] ,
      have at_least : Ici a ⊆ { n | s n ∉ Iio (s m₀) } := by rwa ← eq ,
      exact at_top.sets_of_superset (mem_at_top a) at_least , } ,
    exact ⟨m₀, λ b hb, h_incr hb⟩ , },
  simpa only [and_not_self, not_eventually_false] using yes.and no,
end

[Kalle Kytölä]

What I originally wanted to ask regarding this lemma is whether it was (1) missing deliberately, (2) missing not deliberately, or (3) deliberately not missing. I'm still slightly unsure about the conclusion...

(In my own level of the game I can use an arbitrarily pedestrian version of this, but I of course greatly appreciate the improvements of Kevin and Patrick.)

[Yaël Dillies]

Random note: it's cleaner to call instances using \fl the type of the instance \fr than by its name _inst_1 which is susceptible to change. In general French quotes allow you to make Lean fetch assumptions (or hypotheses, however you want to call them) from the local context without having to name them. It's mostly useful for instances as they are basically the only hypotheses you don't get to name.

[Mario Carneiro]

you can also name them when you need to reference them (which is almost never)

[Mario Carneiro]

In particular in this case you should write is_trichotomous σ (<) instead of using _inst_1

[Mario Carneiro]

and ne_bot (@at_top σ _)

[Yaël Dillies]

Isn't also ne_bot (@at_top \sigma \fl preorder \alpha\fr) the same as non_trivial \alpha?

[Mario Carneiro]

No, the at_top filter is nontrivial iff there is no top element

[Mario Carneiro]

that is no_top_order

[Patrick Massot]

Kalle, is the following sufficient for your purposes?

lemma tendsto_ge_of_incr {σ τ : Type*} [semilattice_sup σ] [linear_order τ]
   [topological_space τ] [order_topology τ]
  {s : σ → τ} {l : τ} (h_incr : monotone s) (h_lim : tendsto s at_top (𝓝 l)) :
    ∀ n , s n ≤ l :=
begin
  intros m₀ ,
  by_contra over_lim,
  have yes : ∀ᶠ n in at_top, s n ∈ Iio (s m₀),
    from h_lim (Iio_mem_nhds $ not_le.1 over_lim),
  have no : ∀ᶠ n in at_top, s n ∉ Iio (s m₀),
  { suffices : ∃ a, ∀ n ≥ a, s m₀ ≤ s n,
    { cases this with a ha ,
      have eq : { n | s m₀ ≤ s n } = { n | s n ∉ Iio (s m₀) }
        := by simp only [mem_Iio, not_lt] ,
      have at_least : Ici a ⊆ { n | s n ∉ Iio (s m₀) } := by rwa ← eq ,
      exact at_top.sets_of_superset (mem_at_top a) at_least , } ,
    exact ⟨m₀, λ b hb, h_incr hb⟩ , },
  haveI : nonempty σ := ⟨m₀⟩,
  haveI : (at_top : filter σ).ne_bot := infer_instance,
  simpa only [and_not_self, not_eventually_false] using yes.and no,
end

[Kalle Kytölä]

Patrick Massot said:

Kalle, is the following sufficient for your purposes?

It certainly is enough to cover the cases I had in mind!

But even with this, library_search only finds the real increasing case but not the ennreal case or the real decreasing case. All of these of course work with any of the proposed versions so far. But I can imagine a user wanting to find the statement by a tactic (instead of the docs, where the typeclass inference is left to the user), and I don't understand why it is found in one case and not the other(s), although the generality is enough for all... Could it be that I don't have enough imports for the searches below?

import topology.instances.real
import topology.instances.ennreal
import init.algebra.classes
import topology.algebra.ordered.basic

open set
open filter
open_locale topological_space

@[simp]
lemma filter.not_eventually_false {α : Type*} (f : filter α) [ne_bot f] : ¬ (∀ᶠ x in f, false) :=
λ h, ne_bot.ne' (eventually_false_iff_eq_bot.mp h)

open filter
lemma tendsto_ge_of_incr {σ τ : Type*} [semilattice_sup σ] [linear_order τ]
   [topological_space τ] [order_topology τ]
  {s : σ → τ} {l : τ} (h_incr : monotone s) (h_lim : tendsto s at_top (𝓝 l)) :
    ∀ n , s n ≤ l :=
begin
  intros m₀ ,
  by_contra over_lim,
  have yes : ∀ᶠ n in at_top, s n ∈ Iio (s m₀),
    from h_lim (Iio_mem_nhds $ not_le.1 over_lim),
  have no : ∀ᶠ n in at_top, s n ∉ Iio (s m₀),
  { suffices : ∃ a, ∀ n ≥ a, s m₀ ≤ s n,
    { cases this with a ha ,
      have eq : { n | s m₀ ≤ s n } = { n | s n ∉ Iio (s m₀) }
        := by simp only [mem_Iio, not_lt] ,
      have at_least : Ici a ⊆ { n | s n ∉ Iio (s m₀) } := by rwa ← eq ,
      exact at_top.sets_of_superset (mem_at_top a) at_least , } ,
    exact ⟨m₀, λ b hb, h_incr hb⟩ , },
  haveI : nonempty σ := ⟨m₀⟩,
  haveI : (at_top : filter σ).ne_bot := infer_instance,
  simpa only [and_not_self, not_eventually_false] using yes.and no,
end

lemma tendsto_ge_of_incr_R' (s : ℕ → ℝ) (l : ℝ) (incr : monotone s) (lim : tendsto s at_top (𝓝 l)) :
    ∀ n , s(n) ≤ l := by library_search --works

lemma tendsto_ge_of_decr_R' (s : ℕ → ℝ) (l : ℝ) (decr : @monotone ℕ (order_dual ℝ) _ _ s) (lim : tendsto s at_top (𝓝 l)) :
    ∀ n , l ≤ s(n) := by library_search --does not work

lemma tendsto_ge_of_incr_ennreal' (s : ℕ → ennreal) (l : ennreal) (incr : monotone s) (lim : tendsto s at_top (𝓝 l)) :
  ∀ n , s(n) ≤ l := by library_search --does not work

In any case this (and other) formulation(s) close the goals when inserted above. So in that sense they work.

[Heather Macbeth]

@Kalle Kytölä, I noticed the same gap today (and searching back in Zulip I found this previous discussion). I also was surprised that it was missing!

I have just PR'd it, #7983. The lemma monotone.ge_of_tendsto is my version of your tendsto_ge_of_incr. But the proof is a bit shorter ;-). Here it is in your notation:

import topology.algebra.ordered.basic

open filter
open_locale topological_space

lemma tendsto_ge_of_incr {σ τ : Type*} [nonempty σ] [semilattice_sup σ]
  [linear_order τ] [topological_space τ] [order_topology τ]
  {s : σ → τ} {l : τ} (h_incr : monotone s) (h_lim : tendsto s at_top (𝓝 l)) :
  ∀ n, s n ≤ l :=
λ n, ge_of_tendsto h_lim ((eventually_ge_at_top n).mono (λ _ hxy, h_incr hxy))

[Kalle Kytölä]

A bit shorter? Wow!

Thanks a lot @Heather Macbeth! I tended to believe it would be useful in mathlib, and if your PR lands there before I finish my current exercise, I will be able to use it :smile:.