## Stream: new members

### Topic: mathlib monotone definition

#### Dan Stanescu (Jul 10 2020 at 17:41):

Just reading the statement of the lemma below may make most people frown. Is there a reason not to change the definition of monotone to include monotonically decreasing sequences in mathlib? Also, could someone please teach me how to use the order_dual tag to produce the proper result in this case?

import data.real.basic

noncomputable theory
-- reciprocals of nats
def recipr_seq (n : ℕ) : ℝ := ( 1/(n+1) : ℝ )

lemma not_mono_recipr : ¬ monotone recipr_seq :=
begin
unfold monotone,
push_neg,
use [1,2],
split,
{ linarith, },
{ unfold recipr_seq, norm_num, },
done

end


#### Kevin Buzzard (Jul 10 2020 at 18:00):

Aah, the convention is that mono is order-preserving

#### Kevin Buzzard (Jul 10 2020 at 18:00):

I think there's antimono?

#### Alex J. Best (Jul 10 2020 at 18:00):

The order dual way would be

import data.real.basic

noncomputable theory
-- reciprocals of nats
def recipr_seq (n : ℕ) : order_dual ℝ := ( 1/(n+1) : ℝ )

lemma mono_recipr : monotone (recipr_seq) :=
begin
intros x y h,
dsimp [recipr_seq],
sorry,
end


#### Alex J. Best (Jul 10 2020 at 18:02):

But antimono is way less confusing looking :wink:

#### Reid Barton (Jul 10 2020 at 18:04):

This will probably get very confusing if you try to use it, yes

#### Dan Stanescu (Jul 10 2020 at 18:05):

Alex J. Best said:

The order dual way would be

import data.real.basic

noncomputable theory
-- reciprocals of nats
def recipr_seq (n : ℕ) : order_dual ℝ := ( 1/(n+1) : ℝ )

lemma mono_recipr : monotone (recipr_seq) :=
begin
intros x y h,
dsimp [recipr_seq],
sorry,
end


This is something I tried, but it still gives the same goal as without order_dual:

xy: ℕ
h: x ≤ y
⊢ 1 / (↑x + 1) ≤ 1 / (↑y + 1)


#### Alex J. Best (Jul 10 2020 at 18:05):

Right, but now \le means the opposite of the usual one on \R

What Reid said

#### Dan Stanescu (Jul 10 2020 at 18:11):

Kevin Buzzard said:

I think there's antimono?

There's at least antimono_seq_of_seq that I could find in filter/bases.

Thank you all!

#### Reid Barton (Jul 10 2020 at 18:13):

We had "fun" with this in the category theory library for a while.

#### Yury G. Kudryashov (Jul 11 2020 at 03:49):

We don't have a definition of antimono in mathlib. One of the ways to state this is ((≤) ⇒ (≥)) recipr_seq recipr_seq.

#### Dan Stanescu (Jul 11 2020 at 14:34):

Thanks Yury, I'll give this a try. But isn't this basically the same as order_dual? At any rate, I gave order_dual a try the other day and apparently there are quite some problems. I was also using positivity of the terms and linarith was somehow getting confused. Let alone my own confusion.

What are the cons to having an additional definition, something like monotone_seq, to leave monotone alone but still use a language that users will understand at first glance?

#### Reid Barton (Jul 11 2020 at 14:44):

Dan Stanescu said:

Thanks Yury, I'll give this a try. But isn't this basically the same as order_dual? At any rate, I gave order_dual a try the other day and apparently there are quite some problems. I was also using positivity of the terms and linarith was somehow getting confused. Let alone my own confusion.

In some sense it is basically the same, but the difference is that you write a ≤ b and a ≥ b to mean $a \le b$ and $a \ge b$, as opposed to writing a ≤ b and a ≤ b but using different instances of has_le real. Otherwise they are probably definitionally equal.

#### Reid Barton (Jul 11 2020 at 14:44):

Dan Stanescu said:

What are the cons to having an additional definition, something like monotone_seq, to leave monotone alone but still use a language that users will understand at first glance?

What additional definition do you have in mind?

#### Patrick Massot (Jul 11 2020 at 14:53):

I really don't know what started this monotone crazyness. Maybe it's just that English is a broken language. This issue simply don't exist in French.

#### Patrick Massot (Jul 11 2020 at 14:54):

In French monotone mean either non-increasing or non-decreasing. And of course we don't have those non-* crazyness either, we say "croissante, strictement croissante, décroissante, strictement décroissante".

#### Alex J. Best (Jul 11 2020 at 15:08):

In non-lean english monotone means monotone increasing or decreasing too, even the venerable wikipedia agrees: "In mathematics, a monotonic function (or monotone function) is a function between ordered sets that preserves or reverses the given order."

#### Patrick Massot (Jul 11 2020 at 15:14):

Ok, so we'll need a fun refactor at some point.

#### Reid Barton (Jul 11 2020 at 15:20):

I think this is true in high school algebra but not really true otherwise.

#### Patrick Massot (Jul 11 2020 at 15:35):

What is true? What Alex says?

#### Dan Stanescu (Jul 11 2020 at 15:39):

Patrick Massot said:

In French monotone mean either non-increasing or non-decreasing. And of course we don't have those non-* crazyness either, we say "croissante, strictement croissante, décroissante, strictement décroissante".

Patrick, the terminology is the same in both languages. The "problem" I see is that the mathlib definition does not agree with either language. In mathlib, a monotone sequence is only monotone increasing.

#### Dan Stanescu (Jul 11 2020 at 15:40):

So if one has a monotonically decreasing sequence, one needs to do extra acrobatics to obtain a proof that it is monotone.

#### Dan Stanescu (Jul 11 2020 at 15:44):

These acrobatics involve using order_dual and are somehow like changing the sign, for example. So one has a decreasing sequence going to 1, change the sign to get an increasing sequence into "-1", and you can much more easily prove the latter one is monotone.

#### Reid Barton (Jul 11 2020 at 15:45):

Patrick Massot said:

What is true? What Alex says?

#### Reid Barton (Jul 11 2020 at 15:46):

I'm also skeptical that "monotone increasing or monotone decreasing" is a useful concept

#### Patrick Massot (Jul 11 2020 at 15:47):

Dan, it seems Alex and Reid disagree with you.

#### Reid Barton (Jul 11 2020 at 15:49):

Whether it's useful in general or not, surely what you want to prove about the original recipr_seq is that it's monotone decreasing, not that it is monotone-increasing-or-monotone-decreasing.

#### Dan Stanescu (Jul 11 2020 at 15:49):

Patrick Massot said:

Dan, it seems Alex and Reid disagree with you.

It seems to me that Alex agrees 100%.

#### Alex J. Best (Jul 11 2020 at 15:49):

I'm sure people who study order theory or something similar use the stricter definition, but I'd put the cutoff of people using the strictly increasing or decreasing definition way above "high school algebra", I'm sure it includes undergraduate analysis for one. For instance I just checked baby rudin for example: where he has

4.28 Definition Let f be real on (a, b). Then f is said to be monotonically
increasing on (a, b) if a < x < у < b implies f(x) <,fiy). If the last inequality
is reversed, we obtain the definition of a monotonically decreasing function. The
class of monotonic functions consists of both the increasing and the decreasing
functions.

#### Patrick Massot (Jul 11 2020 at 15:50):

Sorry Dan, I meant Reid indeed.

#### Dan Stanescu (Jul 11 2020 at 15:50):

Reid Barton said:

Whether it's useful in general or not, surely what you want to prove about the original recipr_seq is that it's monotone decreasing, not that it is monotone-increasing-or-monotone-decreasing.

I want to prove that it is a monotone sequence, as an input for Bolzano-Weierstrass.

#### Alex J. Best (Jul 11 2020 at 15:51):

Its not that I'm personally invested in the definition of monotone, but trying to follow the principle of least astonishment seems like a good idea to me :slight_smile:

#### Reid Barton (Jul 11 2020 at 15:52):

But for me that is what the current definition achieves already.

#### Patrick Massot (Jul 11 2020 at 15:52):

It seems we are mixing two debates. The debate "monotone means increasing" and whether increasing is meant as strictly increasing

#### Reid Barton (Jul 11 2020 at 15:52):

I think everyone here agrees that "monotone" is about $\le$ and not $<$

#### Patrick Massot (Jul 11 2020 at 15:52):

Reid, would you be confused if we replaced monotone by non-decreasing everywhere?

#### Reid Barton (Jul 11 2020 at 15:53):

Well, it's kind of a weird name in the context of partial orders

#### Dan Stanescu (Jul 11 2020 at 15:53):

I didn't mean to produce an uproar. The point is, Bolzano-Weierstrass for sequences is the most useful tool in showing convergence of sequences generated by numerical approximations. For this simple example recipr_seq though, I can't get to prove that it's monotone.

#### Dan Stanescu (Jul 11 2020 at 15:54):

Unless I do special acrobatics which really are not related to the case under scrutiny.

#### Patrick Massot (Jul 11 2020 at 15:54):

I don't get the link between Bolzano-Weirstrass and monotone sequences.

#### Reid Barton (Jul 11 2020 at 15:54):

since for partial orders "$y$ is not less than $x$" is not the same as "$x \le y$"

#### Patrick Massot (Jul 11 2020 at 15:55):

Oh, you're complaining about the non-* crazyness? This is indeed crazy.

#### Reid Barton (Jul 11 2020 at 15:55):

order_preserving would be okay, I think.

#### Patrick Massot (Jul 11 2020 at 15:56):

That one indeed avoids the issue, and can come together with order_reversing.

#### Reid Barton (Jul 11 2020 at 15:57):

and strictly_order_preserving for the < counterpart works as well

#### Reid Barton (Jul 11 2020 at 15:57):

and, the pair is even French-compatible

#### Dan Stanescu (Jul 11 2020 at 15:58):

Patrick Massot said:

I don't get the link between Bolzano-Weirstrass and monotone sequences.

BW uses the monotone subsequence theorem (every sequence has a monotone subsequence), doesn't it?

#### Patrick Massot (Jul 11 2020 at 16:01):

Certainly not in the BW we have in mathlib.

#### Patrick Massot (Jul 11 2020 at 16:02):

Which has no order in sight.

#### Patrick Massot (Jul 11 2020 at 16:03):

If you ask mathlib about BW for segments of real numbers, it will go through the fact that the uniform structure on R has a countable basis, but not through the order relation on R :grinning:

#### Dan Stanescu (Jul 11 2020 at 16:05):

@Patrick Massot OK, there are two flavors of BW (for sequences and for sets) and I confess I didn't look in mathlib yet as my internet is on and off today.
But the monotone convergence theorem then (a bounded monotone sequence converges). Which I don't know if it is in mathlib or not.

#### Patrick Massot (Jul 11 2020 at 16:10):

I don't know what you call BW for sets.

#### Dan Stanescu (Jul 11 2020 at 16:14):

Patrick Massot said:

I don't know what you call BW for sets.

The way I know it is: every bounded infinite subset of \R has an accumulation point in \R.

#### Dan Stanescu (Jul 12 2020 at 18:59):

Patrick Massot said:

Sorry Dan, I meant Reid indeed.

@Patrick Massot Patrick, it turns out your message also shows that you agree (and Alex, and Rudin's book, and Wikipedia, and the common usage of the term, and so on). Quoting you: "In French monotone mean either non-increasing or non-decreasing." That's exactly what I'm advocating. In other words, your definition of monotone, just like mine, means that the sequence def x (n : ℕ) : ℝ := ( 1/(n+1) : ℝ )  should be monotone (because it is non-increasing). I find it unfortunate (and confusing) that the mathlib definition monotone works differently. With mathlib's definition, one can prove that this sequence is not monotone. Just scroll back to the top of this stream.

I came back to this because I think it is important. Hold on, I'll try to explain why in a subsequent message.

#### Dan Stanescu (Jul 12 2020 at 19:05):

Here is the point I want to make here, for whatever it's worth. This will be a somewhat longer message, so beware!

Lean + mathlib are interesting from many perspectives. Not the least of them is the fact that they offer a great educational tool. I have read students' arguments about how much Lean proofs help them focus, thus diminishing the effects of ADHD. And we all know the impact the NNG had. If this is worth pursuing then, it is probably a good idea to keep the API as close as possible to standard terminology. It is only with mathlib's monotone that I found (so far) this is not the case. We can't teach students monotone means something and have them come to mathlib to show them that monotone means something else. Well, we can, but is it desirable?
Furthermore, a great API will help many more people adopt Lean, or at the very least try it out. For example, people working in numerical methods, which is where I come from. There isn't any contribution in numerical analysis in mathlib yet, AFAIK. In numerics we usually care only about \R and \C for the most part, that is true. But nobody I know would ever consider 1/n to not be monotone. I'm an engineer by training, not a mathematician; this is bad for me in this context, I totally agree that there may be lots of things for which I don't have a mathematician's perspective. But it is good for most of you, as it gives you a perspective from the other side of the fence.
In this particular case, there are alternatives that would keep the current gains in mathlib without sacrifice for the friendliness of the interface. For example, as @Patrick Massot and @Reid Barton suggest, what is currently monotone in mathlib should rather be order_preserving. Maybe monotone could then be changed to reflect the common meaning. Also, we should ideally have tendsto_of_monotone taking care of all monotone sequences (unless I'm wrong, it currently can only handle non-decreasing). Or have some alternative, like tendsto_of_non_increasing and tendsto_of_non_decreasing.
To wrap up, this is not about pointing fingers and/or blaming past decisions. It's about possibly changing for the better. Again, I may not have the best perspective, so this is rather something to be considered by long-time members of the community. If any change is deemed worth pursuing, I hope it can be largely done through software.

#### Reid Barton (Jul 12 2020 at 19:15):

I still don't think this "increasing or decreasing" meaning of monotone is really "standard", or better, it is standard in some fields, but not in others.

#### Reid Barton (Jul 12 2020 at 19:16):

I would suggest the following changes:

• rename monotone to order_preserving
• add monotonic (not monotone) with the increasing-or-decreasing definition

#### Reid Barton (Jul 12 2020 at 19:17):

What's tendsto_of_monotone?

#### Anatole Dedecker (Jul 12 2020 at 19:19):

https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#tendsto_of_monotone

#### Reid Barton (Jul 12 2020 at 19:20):

Thanks, too new for my local mathlib.

#### Alex J. Best (Jul 12 2020 at 19:22):

The issue I'm having is I can't think of another good name for "order preserving or reversing", but there are other good names for the strict version, like order_hom or isotone/isotonic. Having monotonic and monotone be different sounds very confusing to me.

#### Reid Barton (Jul 12 2020 at 19:23):

I'm suggesting having nothing named monotone.

#### Alex J. Best (Jul 12 2020 at 19:23):

Oh my bad I misread, I agree with you then!

#### Reid Barton (Jul 12 2020 at 19:24):

This is an example of why I'm a little bit skeptical about the utility of the increasing-or-decreasing notion for formalization--the statement of tendsto_of_monotone is false with that version; you can add "converges to $-\infty$" as another option but then the statement is a bit weaker if you know the sequence is order-preserving.

#### Reid Barton (Jul 12 2020 at 19:25):

My sense is that in practice you don't just know that the sequence is increasing-or-decreasing, you know which one it is.

#### Reid Barton (Jul 12 2020 at 19:26):

And sometimes it matters which one it is, while other times it doesn't

#### Reid Barton (Jul 12 2020 at 19:28):

Or you want to use the fact that a monotone bounded sequence converges. Well, really you want to use the fact that a monotone increasing sequence that's bounded above converges, otherwise you have to prove an unnecessary side condition (bounded below).

#### Reid Barton (Jul 12 2020 at 19:28):

That's why my reaction to your original example was that you really want to prove the sequence is monotone decreasing

#### Alex J. Best (Jul 12 2020 at 19:28):

What about some results like strict monotonic implies has an inverse, or non-zero first derivative implies strict monotonic for functions on subsets of reals.

#### Reid Barton (Jul 12 2020 at 19:29):

Sure, it sometimes happens this way too

#### Alex J. Best (Jul 12 2020 at 19:29):

I do agree also though that if you can prove somethings derivative is nonvanishing you can probably prove whether or not it is positive or negative.

#### Reid Barton (Jul 12 2020 at 19:30):

I just think that, on balance, the "monotone increasing" notion is far more useful (already hundreds of uses of monotone in mathlib) than the "increasing or decreasing" notion, so it should not be too surprising that monotone currently means the former

#### Dan Stanescu (Jul 12 2020 at 19:31):

Reid Barton said:

That's why my reaction to your original example was that you really want to prove the sequence is monotone decreasing

Part of the problem is that I don't think there's anything for monotone decreasing sequences in mathlib. It's as if monotone decreasing sequences don't exist.

#### Reid Barton (Jul 12 2020 at 19:32):

Sort of like how $A \subset B$ almost surely means "$A$ is a subset of $B$" rather than "$A$ is a strict subset of $B$" (even though Lean thinks it means the second one) simply because the former notion is far more frequent than the latter.

#### Dan Stanescu (Jul 12 2020 at 19:33):

So we must have some mechanisms for monotone decreasing sequences also.

#### Patrick Massot (Jul 12 2020 at 20:00):

Dan Stanescu said:

So we must have some mechanisms for monotone decreasing sequences also.

This is completely independent from the terminology question. Of course we should also prove lemmas for decreasing sequences.

#### Patrick Massot (Jul 12 2020 at 20:01):

Side note about your long message: as you know I'm using Lean for very elementary teaching, but the monotone thing is irrelevant here because I redefine everything (there is no way I can use our filter based topology library with my first year undergrads.

#### Reid Barton (Aug 28 2020 at 21:07):

Reid Barton said:

I would suggest the following changes:

• rename monotone to order_preserving
• add monotonic (not monotone) with the increasing-or-decreasing definition

So I came back to this and I'm concerned about the practicality of the change I proposed above. Here's a small sample of the 699 lines in mathlib matching monotone, just the lines from a single file topology.uniform_space.basic.

src/topology/uniform_space/basic.lean:theorem monotone_comp_rel [preorder β] {f g : β → set (α×α)}
src/topology/uniform_space/basic.lean:  (hf : monotone f) (hg : monotone g) : monotone (λx, (f x) ○ (g x)) :=
src/topology/uniform_space/basic.lean:    apply monotone_comp_rel; exact monotone_id,
src/topology/uniform_space/basic.lean:(mem_lift'_sets $monotone_comp_rel monotone_id monotone_id).mp this src/topology/uniform_space/basic.lean:⟨t', ht', ht'₁, subset.trans (monotone_comp_rel monotone_id monotone_id ht'₂) ht₂⟩ src/topology/uniform_space/basic.lean:theorem uniformity_lift_le_swap {g : set (α×α) → filter β} {f : filter β} (hg : monotone g) src/topology/uniform_space/basic.lean:lemma uniformity_lift_le_comp {f : set (α×α) → filter β} (h : monotone f) : src/topology/uniform_space/basic.lean: exact monotone_comp_rel monotone_id monotone_id, src/topology/uniform_space/basic.lean: exact (assume x, monotone_comp_rel monotone_const$ monotone_comp_rel monotone_id monotone_id),
src/topology/uniform_space/basic.lean:    exact (assume x, monotone_comp_rel monotone_id monotone_const),
src/topology/uniform_space/basic.lean:      monotone_principal.comp (monotone_comp_rel monotone_const monotone_id)
src/topology/uniform_space/basic.lean:      (assume s, monotone_comp_rel monotone_const monotone_id)
src/topology/uniform_space/basic.lean:      (assume s, monotone_comp_rel monotone_id monotone_const)
src/topology/uniform_space/basic.lean:lemma lift_nhds_left {x : α} {g : set α → filter β} (hg : monotone g) :
src/topology/uniform_space/basic.lean:    exact (filter.lift_assoc $monotone_principal.comp$ monotone_preimage.comp monotone_preimage )
src/topology/uniform_space/basic.lean:lemma lift_nhds_right {x : α} {g : set α → filter β} (hg : monotone g) :
src/topology/uniform_space/basic.lean:    map_lift_eq2 $hg.comp monotone_preimage src/topology/uniform_space/basic.lean: exact monotone_principal.comp (monotone_prod monotone_const monotone_id), src/topology/uniform_space/basic.lean: exact (monotone_lift' monotone_const$ monotone_lam $src/topology/uniform_space/basic.lean: assume x, monotone_prod monotone_id monotone_const) src/topology/uniform_space/basic.lean: { intro s, exact monotone_prod monotone_const monotone_preimage }, src/topology/uniform_space/basic.lean: { intro t, exact monotone_prod monotone_preimage monotone_const } src/topology/uniform_space/basic.lean: exact monotone_prod monotone_preimage monotone_preimage src/topology/uniform_space/basic.lean: exact monotone_prod monotone_preimage monotone_preimage src/topology/uniform_space/basic.lean: exact monotone_inter (monotone_prod monotone_preimage monotone_preimage) monotone_const src/topology/uniform_space/basic.lean: monotone_comp_rel monotone_id$ monotone_comp_rel monotone_id monotone_id).mp (comp_le_uniformity3 hd) in
src/topology/uniform_space/basic.lean:    exact monotone_comp_rel monotone_id monotone_id
src/topology/uniform_space/basic.lean:      repeat { exact monotone_comp_rel monotone_id monotone_id }
src/topology/uniform_space/basic.lean:    refine ⟨i, m', hm', λ z hz, h (monotone_comp_rel monotone_id monotone_const mm' _)⟩,


As you can see, monotone appears an average of many times per line. Now order_preserving is quite a few characters longer than monotone and I don't really want to reflow a bunch of proofs here and throughout the rest of mathlib.

#### Patrick Massot (Aug 28 2020 at 21:09):

What about shortening it? order_pre? ord_pre?

#### Reid Barton (Aug 28 2020 at 21:10):

I was going to suggest, of all things, increasing as a possibility

#### Reid Barton (Aug 28 2020 at 21:10):

If we're going for cryptic, mono is another possibility. But it could be expanded to other things.

#### Patrick Massot (Aug 28 2020 at 21:11):

I thought increasing meant something else in English. I would certainly vote for increasing from a French speaking perspective.

#### Patrick Massot (Aug 28 2020 at 21:12):

In any case it's great to see you have courage for such an endeavor in addition to the great nat.pow quest!

#### Reid Barton (Aug 28 2020 at 21:13):

I'm slightly embarrassed to admit I'm currently interested in formalizing a theorem whose English formulation uses the word "monotone" with the "increasing or decreasing" meaning.

#### Reid Barton (Aug 28 2020 at 21:14):

Another option, that nobody will have heard of, is isotone

#### Reid Barton (Aug 28 2020 at 21:15):

I think the situation with "increasing" in English is that it is ambiguous

#### Reid Barton (Aug 28 2020 at 21:15):

but, it wouldn't be the only such word for which we pick a meaning in mathlib

#### Reid Barton (Aug 28 2020 at 21:22):

Anyways, I'm in no great hurry here so I'll just say my current preference is for increasing but give people a few days to chime in with opinions/suggestions.

#### Mario Carneiro (Aug 28 2020 at 21:34):

ord_hom seems abstract but unambiguous

#### Mario Carneiro (Aug 28 2020 at 21:35):

I would suggest reserving mono (or le_of_le) for the idiom x <= y -> f x <= f y without any abbreviation

#### Dan Stanescu (Aug 28 2020 at 21:52):

Reid Barton said:

Anyways, I'm in no great hurry here so I'll just say my current preference is for increasing but give people a few days to chime in with opinions/suggestions.

Probably the only question is whether the ambiguity in increasing versus non_decreasing ororder_preserving, say, may lead again to reconsideration later on - just as the choice of monotone turned out to do. Either way we chose though, restructuring headache (which I can't evaluate for difficulty) aside, it will be much more easily understood across the board.

#### Reid Barton (Aug 28 2020 at 21:59):

"nondecreasing" isn't really appropriate because the order may be partial--probably the most common choice of order by far is the subset relation (or something closely related). But we also want to choose a name that makes sense for things like nat -> real or real -> real. That's part of what makes choosing a good name difficult.

#### Mario Carneiro (Aug 28 2020 at 22:06):

Can we maybe compromise on "monotonic means increasing or decreasing" instead? For example calling this inc_dec or something

#### Mario Carneiro (Aug 28 2020 at 22:07):

that seems more sensible than changing a definition that is already very useful and used widely in mathlib

#### Reid Barton (Aug 28 2020 at 22:27):

Yes, that might be the better option

#### Aaron Anderson (Aug 29 2020 at 00:23):

Mario Carneiro said:

ord_hom seems abstract but unambiguous

sort of ambiguous, you could still have ord_hom be a rel_hom for <= or <. One of those is monotone, the other is strict_mono

#### Mario Carneiro (Aug 29 2020 at 00:28):

I don't think it matters, it will either be obvious from context or the statement, or it can be disambiguated with a strict

Last updated: May 11 2021 at 00:31 UTC