feat(order/monotone/monovary): Monovarying functions are jointly monotone

[YaelDillies]

This PR justifies the understanding of monovary f g as "f and g are jointly monotone". Precisely, it shows that two functions monovary iff there is a linear order on their domain that makes them monotone simultaneously.

---

• depends on: [Merged by Bors] - feat(data/prod/basic): prod.lex is trichotomous #17931

I've left a todo for the version of the lemma that replaces "two" by "an arbitrary number of". I don't need it, but it sure would be very fun to prove!

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(data/prod/basic): prod.lex is trichotomous #17931
  By Dependent Issues (🤖). Happy coding!

[eric-wieser]

This feels like it might be a pretty annoying spelling if ι already has an order.

What are your thoughts on making a with_mono_vary_order f g ι type synonym and instead stating this as something like

Suggested change

	monovary_on f g s ↔ ∃ [linear_order ι], by exactI monotone_on f s ∧ monotone_on g s :=
	monovary_on f g s ↔ monotone_on (f ∘ of_mvo f g) (of_mvo f g ⁻¹' s) ∧ monotone_on (g ∘ of_mvo f g) (of_mvo f g⁻¹' s) :=

[YaelDillies]

I thought about it too, but I would need four different type synonyms for the lemmas here, so I'm not convinced. The use case is deducing the Chebyshev sum inequality (pretty general and stated in terms of monovary in #13187) from the FKG inequality, where everything has an order (and is thus a priori less general). So the only point at which I will have this extra linear_order ι instance will be locally in the proof of Chebyshev, where there is no pre-existing order on ι.

[eric-wieser]

Why do you need four type synonyms?

[YaelDillies]

because the same type won't work for all four lemmas (I would need to insert order_dual in places).

[eric-wieser]

I'd probably argue that at that point you don't need all four lemmas; only the two(?) that don't mention order_dual at all.

[YaelDillies]

I don't think that's an improvement over the current situation given my use case and the todo I am leaving (would you want yet another type synonym for families of functions?).

[YaelDillies]

In fact, I see it as such:

• If I provide a type synonym, I make the choice for the user on what order they want to use (regarding order_dual).
• If the user expands out my ∃ [linear_order ι], ..., they are free to make it a local instance, or place it onto a type synonym (which you indeed can create locally using set and clear_value).

[YaelDillies]

Ported to LeanCamCombi