mathlib monotone definition

Stream: new members

[Dan Stanescu]

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]

Aah, the convention is that mono is order-preserving

[Kevin Buzzard]

I think there's antimono?

[Alex J. Best]

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]

But antimono is way less confusing looking :wink:

[Reid Barton]

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

[Dan Stanescu]

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]

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

[Kevin Buzzard]

What Reid said

[Dan Stanescu]

Kevin Buzzard said:

I think there's antimono?

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

[Dan Stanescu]

Thank you all!

[Reid Barton]

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

[Yury G. Kudryashov]

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

[Dan Stanescu]

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]

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]

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]

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]

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]

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]

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

[Reid Barton]

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

[Patrick Massot]

What is true? What Alex says?

[Dan Stanescu]

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]

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

[Dan Stanescu]

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]

Patrick Massot said:

What is true? What Alex says?

Yes. Compare https://en.wikipedia.org/wiki/Monotonic_function#Monotonicity_in_order_theory, https://ncatlab.org/nlab/show/monotone+function.

[Reid Barton]

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

[Patrick Massot]

Dan, it seems Alex and Reid disagree with you.

[Reid Barton]

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]

Patrick Massot said:

Dan, it seems Alex and Reid disagree with you.

It seems to me that Alex agrees 100%.

[Alex J. Best]

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]

Sorry Dan, I meant Reid indeed.

[Dan Stanescu]

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]

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]

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

[Patrick Massot]

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

[Reid Barton]

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

[Patrick Massot]

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

[Reid Barton]

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

[Dan Stanescu]

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]

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

[Patrick Massot]

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

[Reid Barton]

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

[Patrick Massot]

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

[Reid Barton]

order_preserving would be okay, I think.

[Patrick Massot]

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

[Reid Barton]

and strictly_order_preserving for the < counterpart works as well

[Reid Barton]

and, the pair is even French-compatible

[Dan Stanescu]

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]

Certainly not in the BW we have in mathlib.

[Patrick Massot]

Which has no order in sight.

[Patrick Massot]

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]

@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]

We have https://leanprover-community.github.io/mathlib_docs/topology/sequences.html#tendsto_subseq_of_bounded and https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#tendsto_of_monotone

[Patrick Massot]

or maybe you prefer https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#tendsto_at_top_csupr

[Patrick Massot]

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

[Dan Stanescu]

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]

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]

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]

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]

I would suggest the following changes:

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

[Reid Barton]

What's tendsto_of_monotone?

[Anatole Dedecker]

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

[Reid Barton]

Thanks, too new for my local mathlib.

[Alex J. Best]

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]

I'm suggesting having nothing named monotone.

[Alex J. Best]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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

[Alex J. Best]

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]

Sure, it sometimes happens this way too

[Alex J. Best]

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]

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]

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]

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]

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

[Patrick Massot]

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]

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]

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]

What about shortening it? order_pre? ord_pre?

[Reid Barton]

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

[Reid Barton]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

ord_hom seems abstract but unambiguous

[Mario Carneiro]

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

[Dan Stanescu]

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]

"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]

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

[Mario Carneiro]

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

[Reid Barton]

Yes, that might be the better option

[Aaron Anderson]

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]

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