Monotonicity #
This file defines (strictly) monotone/antitone functions. Contrary to standard mathematical usage, "monotone"/"mono" here means "increasing", not "increasing or decreasing". We use "antitone"/"anti" to mean "decreasing".
Definitions #
monotone f
: A functionf
between two preorders is monotone ifa ≤ b
impliesf a ≤ f b
.antitone f
: A functionf
between two preorders is antitone ifa ≤ b
impliesf b ≤ f a
.monotone_on f s
: Same asmonotone f
, but for alla, b ∈ s
.antitone_on f s
: Same asantitone f
, but for alla, b ∈ s
.strict_mono f
: A functionf
between two preorders is strictly monotone ifa < b
impliesf a < f b
.strict_anti f
: A functionf
between two preorders is strictly antitone ifa < b
impliesf b < f a
.strict_mono_on f s
: Same asstrict_mono f
, but for alla, b ∈ s
.strict_anti_on f s
: Same asstrict_anti f
, but for alla, b ∈ s
.
Main theorems #
monotone_nat_of_le_succ
,monotone_int_of_le_succ
: Iff : ℕ → α
orf : ℤ → α
andf n ≤ f (n + 1)
for alln
, thenf
is monotone.antitone_nat_of_succ_le
,antitone_int_of_succ_le
: Iff : ℕ → α
orf : ℤ → α
andf (n + 1) ≤ f n
for alln
, thenf
is antitone.strict_mono_nat_of_lt_succ
,strict_mono_int_of_lt_succ
: Iff : ℕ → α
orf : ℤ → α
andf n < f (n + 1)
for alln
, thenf
is strictly monotone.strict_anti_nat_of_succ_lt
,strict_anti_int_of_succ_lt
: Iff : ℕ → α
orf : ℤ → α
andf (n + 1) < f n
for alln
, thenf
is strictly antitone.
Implementation notes #
Some of these definitions used to only require has_le α
or has_lt α
. The advantage of this is
unclear and it led to slight elaboration issues. Now, everything requires preorder α
and seems to
work fine. Related Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Order.20diamond/near/254353352.
TODO #
The above theorems are also true in ℕ+
, fin n
... To make that work, we need succ_order α
and succ_archimedean α
.
Tags #
monotone, strictly monotone, antitone, strictly antitone, increasing, strictly increasing, decreasing, strictly decreasing
A function f
is strictly monotone if a < b
implies f a < f b
.
Equations
- strict_mono f = ∀ ⦃a b : α⦄, a < b → f a < f b
A function f
is strictly antitone if a < b
implies f b < f a
.
Equations
- strict_anti f = ∀ ⦃a b : α⦄, a < b → f b < f a
Monotonicity on the dual order #
Strictly, many of the *_on.dual
lemmas in this section should use of_dual ⁻¹' s
instead of s
,
but right now this is not possible as set.preimage
is not defined yet, and importing it creates
an import cycle.
Often, you should not need the rewriting lemmas. Instead, you probably want to add .dual
,
.dual_left
or .dual_right
to your monotone
/antitone
hypothesis.
Alias of the reverse direction of antitone_comp_of_dual_iff
.
Alias of the reverse direction of monotone_comp_of_dual_iff
.
Alias of the reverse direction of antitone_to_dual_comp_iff
.
Alias of the reverse direction of monotone_to_dual_comp_iff
.
Alias of the reverse direction of antitone_on_comp_of_dual_iff
.
Alias of the reverse direction of monotone_on_comp_of_dual_iff
.
Alias of the reverse direction of antitone_on_to_dual_comp_iff
.
Alias of the reverse direction of monotone_on_to_dual_comp_iff
.
Alias of the reverse direction of strict_anti_comp_of_dual_iff
.
Alias of the reverse direction of strict_mono_comp_of_dual_iff
.
Alias of the reverse direction of strict_anti_to_dual_comp_iff
.
Alias of the reverse direction of strict_mono_to_dual_comp_iff
.
Alias of the reverse direction of strict_anti_on_comp_of_dual_iff
.
Alias of the reverse direction of strict_mono_on_comp_of_dual_iff
.
Alias of the reverse direction of strict_anti_on_to_dual_comp_iff
.
Alias of the reverse direction of strict_mono_on_to_dual_comp_iff
.
Monotonicity in function spaces #
Monotonicity hierarchy #
These four lemmas are there to strip off the semi-implicit arguments ⦃a b : α⦄
. This is useful
when you do not want to apply a monotone
assumption (i.e. your goal is a ≤ b → f a ≤ f b
).
However if you find yourself writing hf.imp h
, then you should have written hf h
instead.
Monotonicity from and to subsingletons #
Miscellaneous monotonicity results #
Monotonicity under composition #
Monotonicity in linear orders #
Monotonicity in ℕ
and ℤ
#
If α
is a preorder with no maximal elements, then there exists a strictly monotone function
ℕ → α
with any prescribed value of f 0
.
If α
is a preorder with no maximal elements, then there exists a strictly antitone function
ℕ → α
with any prescribed value of f 0
.
If α
is a nonempty preorder with no maximal elements, then there exists a strictly monotone
function ℕ → α
.
If α
is a nonempty preorder with no minimal elements, then there exists a strictly antitone
function ℕ → α
.
If α
is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
monotone function f : ℤ → α
.
If α
is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
antitone function f : ℤ → α
.