Monotonicity of multiplication by positive elements #

This file defines typeclasses to reason about monotonicity of the operations

b ↦ a * b, "left multiplication"
a ↦ a * b, "right multiplication"

We use eight typeclasses to encode the various properties we care about for those two operations. These typeclasses are meant to be mostly internal to this file, to set up each lemma in the appropriate generality.

Less granular typeclasses like OrderedAddCommMonoid, `LinearOrderedField`` should be enough for most purposes, and the system is set up so that they imply the correct granular typeclasses here. If those are enough for you, you may stop reading here! Else, beware that what follows is a bit technical.

Definitions #

In all that follows, α is an orders which has a 0 and a multiplication. Note however that we do not use lawfulness of this action in most of the file. Hence * should be considered here as a mostly arbitrary function α → α → α.

We use the following four typeclasses to reason about left multiplication (b ↦ a * b):

PosMulMono: If a ≥ 0, then b₁ ≤ b₂ → a * b₁ ≤ a * b₂.
PosMulStrictMono: If a > 0, then b₁ < b₂ → a * b₁ < a * b₂.
PosMulReflectLT: If a ≥ 0, then a * b₁ < a * b₂ → b₁ < b₂.
PosMulReflectLE: If a > 0, then a * b₁ ≤ a * b₂ → b₁ ≤ b₂.

We use the following four typeclasses to reason about right multiplication (a ↦ a * b):

MulPosMono: If b ≥ 0, then a₁ ≤ a₂ → a₁ * b ≤ a₂ * b.
MulPosStrictMono: If b > 0, then a₁ < a₂ → a₁ * b < a₂ * b.
MulPosReflectLT: If b ≥ 0, then a₁ * b < a₂ * b → a₁ < a₂.
MulPosReflectLE: If b > 0, then a₁ * b ≤ a₂ * b → a₁ ≤ a₂.

Implications #

As α gets more and more structure, those typeclasses end up being equivalent. The commonly used implications are:

When α is a partial order:
PosMulStrictMono → PosMulMono
MulPosStrictMono → MulPosMono
PosMulReflectLE → PosMulReflectLT
MulPosReflectLE → MulPosReflectLT
When α is a linear order:
- PosMulStrictMono → PosMulReflectLE
- MulPosStrictMono → MulPosReflectLE .
When the multiplication of α is commutative:
- PosMulMono → MulPosMono
- PosMulStrictMono → MulPosStrictMono
- PosMulReflectLE → MulPosReflectLE
- PosMulReflectLT → MulPosReflectLT

Further, the bundled non-granular typeclasses imply the granular ones like so:

OrderedSemiring → PosMulMono
OrderedSemiring → MulPosMono
StrictOrderedSemiring → PosMulStrictMono
StrictOrderedSemiring → MulPosStrictMono

All these are registered as instances, which means that in practice you should not worry about these implications. However, if you encounter a case where you think a statement is true but not covered by the current implications, please bring it up on Zulip!

Notation #

The following is local notation in this file:

α≥0: {x : α // 0 ≤ x}
α>0: {x : α // 0 < x}

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/notation.20for.20positive.20elements for a discussion about this notation, and whether to enable it globally (note that the notation is currently global but broken, hence actually only works locally).