eventually monotone

Stream: maths

[Filippo A. E. Nuccio]

What is the right notion of an eventually monotone function? I would like a slightly stronger version of

lemma tendsto_of_monotone {ι α : Type*} [preorder ι] [topological_space α]
  [conditionally_complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) :
  tendsto f at_top at_top ∨ (∃ l, tendsto f at_top (𝓝 l)) :=

only requiring that ∀ᶠ ⦃a b⦄ in at_top, a ≤ b → f a ≤ f b instead of monotone f which is ∀ ⦃a b⦄, a ≤ b → f a ≤ f b

[Yaël Dillies]

Oooh, that's interesting. I'll have a think.

[Yaël Dillies]

In particular, does it make sense to say that a function is monotone at a filter?

[Filippo A. E. Nuccio]

Well, it seems very natural - I guess it is a question for @Patrick Massot .

[Yaël Dillies]

At any filter? I can't yet see what would be the correct definition.

[Filippo A. E. Nuccio]

Ah well, at any filter I don't know.

[Filippo A. E. Nuccio]

Well, actually yes: it just means that there exists x in the filter where they coincide. Sorry, I take it back - I now understand your question. Let me think more.

[Filippo A. E. Nuccio]

No?

[Yaël Dillies]

Okay, I have an idea, but it works when the topology is on codomain, not the domain :thinking:

[Filippo A. E. Nuccio]

Well, the definition of something holding eventually is

def eventually (p : α → Prop) (f : filter α) : Prop := {x | p x} ∈ f

And I don't see why this can't generalise to

def eventually_pair (p : α x α → Prop) (f g : filter α) : Prop := {x y | p x y } ∈  f ×ᶠ g

[Filippo A. E. Nuccio]

(Of course you can make it more general, I have just tried something for the sake of the discussion).

[Yaël Dillies]

So you want this, right?

def monotone_at (f : α → β) (l : filter (α × α)) : {ab | a ≤ b → f a ≤ f b} ∈ l

[Filippo A. E. Nuccio]

Well, yes; actually my question was really if this had already been implemented.

[Yaël Dillies]

Most probably not

[Filippo A. E. Nuccio]

Strange, no?

[Yaël Dillies]

The thing is we're talking about filters on α, not on α × α.

[Filippo A. E. Nuccio]

Well, but given a pair of filters on α you get a filter on α × α...

[Yaël Dillies]

Yes, but is that the correct definition? The best test would be to prove your lemma above.

[Filippo A. E. Nuccio]

Good point! I'll go ahead and post the result ASAP.

[Yaël Dillies]

I must say I didn't know even to the existence of filters
Filippo A. E. Nuccio said:

Strange, no?

I must say I didn't know even to the existence of filters before joining mathlib, so I can't say what I was expecting. Is eventual monotonicity a well-established concept?

[Yaël Dillies]

Wait, I now remember reading about limits of relations.

[Yaël Dillies]

docs#filter.rtendsto

[Filippo A. E. Nuccio]

Well, before joining mathlib, I had been taught (oddly enough) to run away from filters as fast as possible. So I have no idea about what is "well-estabished".

[Yaël Dillies]

Aaah, I remember. I wrote those docstrings.

[Filippo A. E. Nuccio]

Great!

[Filippo A. E. Nuccio]

You wrote them ?!? Wow, but do you also find the time to breath, from time to time?

[Yaël Dillies]

I was on holidays :sweat_smile:

[Yaël Dillies]

Note however that I'm not sure this is what you want. It is considering functions α → βas relations rel α β. What you want is rather considering relations as functions with twice as much input.

[Yaël Dillies]

I swear I did take a break from Lean! Every day! It's what other people euphemically call "sleep".

[Filippo A. E. Nuccio]

Other people call it addiction... :laughing:

[Filippo A. E. Nuccio]

Thanks, at any rate. I'll have a look and will try to see if I can come up with something useful

[Reid Barton]

My first thought would be that a function is eventually monotone along a filter f if there is a set belonging to f on which it is monotone. Is that the same as eventually_pair with f twice? I think so, right?

[Yaël Dillies]

Yeah, I had the same definition in mind, but I'm not so sure it's the correct definition for a general filter.

[Yaël Dillies]

How is it going, Filippo?

[Yury G. Kudryashov]

I think that the following 3 definitions are equivalent (the first two use a non-existing mono_on):

∀ᶠ s in l.lift' powerset, mono_on f s
∃ᶠ s in l.lift' powerset, mono_on f s
∀ᶠ p in l.prod l, p.1 ≤ p.2 → f p.1 ≤ f p.2

[Yaël Dillies]

Note that I'm introducing monotone_on in #9119, so just assume it exists.

[Yury G. Kudryashov]

The first one says that for some s ∈ l, your function is monotone on any t ⊆ s.

[Yaël Dillies]

I think the last one is what is more intuitively eventual monotonicity.

[Yaël Dillies]

What about

∀ᶠ a in l, ∀ᶠ b in l, a ≤ b → f a ≤ f b

[Reid Barton]

So these are the same basically because mono_on f s is itself monotone (or antitone I guess we're supposed to say) in s

[Yury G. Kudryashov]

Yes.

[Yury G. Kudryashov]

@Yaël Dillies This one in case l = at_top says ∃ N, ∀ n ≥ N, ∃ M, ∀ m ≥ M, n ≤ m → f n ≤ f m.

[Yury G. Kudryashov]

This is not what you want.

[Yury G. Kudryashov]

Because M can depend on N.

[Yaël Dillies]

Well, I'm not sure this isn't what we want. It is definitely looser than your other definitions, but maybe that's enough?

[Reid Barton]

Well it might be enough for something, but it's not what "evenually monotone" means.

[Yury G. Kudryashov]

E.g., you get a different notion if you swap to eventuallys.

[Reid Barton]

e.g. $x + 10 \sin(x)$ has this kind of behavior (that has domain $\mathbb{R}$, but the behavior is the same if you sample finely enough)