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
: Ifa ≥ 0
, thenb₁ ≤ b₂ → a * b₁ ≤ a * b₂
.PosMulStrictMono
: Ifa > 0
, thenb₁ < b₂ → a * b₁ < a * b₂
.PosMulReflectLT
: Ifa ≥ 0
, thena * b₁ < a * b₂ → b₁ < b₂
.PosMulReflectLE
: Ifa > 0
, thena * b₁ ≤ a * b₂ → b₁ ≤ b₂
.
We use the following four typeclasses to reason about right multiplication (a ↦ a * b
):
MulPosMono
: Ifb ≥ 0
, thena₁ ≤ a₂ → a₁ * b ≤ a₂ * b
.MulPosStrictMono
: Ifb > 0
, thena₁ < a₂ → a₁ * b < a₂ * b
.MulPosReflectLT
: Ifb ≥ 0
, thena₁ * b < a₂ * b → a₁ < a₂
.MulPosReflectLE
: Ifb > 0
, thena₁ * 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: - When the multiplication of
α
is commutative:
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).
Typeclass for monotonicity of multiplication by nonnegative elements on the left,
namely b₁ ≤ b₂ → a * b₁ ≤ a * b₂
if 0 ≤ a
.
You should usually not use this very granular typeclass directly, but rather a typeclass like
OrderedSemiring
.
Equations
- PosMulMono α = CovariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 ≤ x2
Instances For
Typeclass for monotonicity of multiplication by nonnegative elements on the right,
namely a₁ ≤ a₂ → a₁ * b ≤ a₂ * b
if 0 ≤ b
.
You should usually not use this very granular typeclass directly, but rather a typeclass like
OrderedSemiring
.
Equations
- MulPosMono α = CovariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 ≤ x2
Instances For
Typeclass for strict monotonicity of multiplication by positive elements on the left,
namely b₁ < b₂ → a * b₁ < a * b₂
if 0 < a
.
You should usually not use this very granular typeclass directly, but rather a typeclass like
StrictOrderedSemiring
.
Equations
- PosMulStrictMono α = CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 < x2
Instances For
Typeclass for strict monotonicity of multiplication by positive elements on the right,
namely a₁ < a₂ → a₁ * b < a₂ * b
if 0 < b
.
You should usually not use this very granular typeclass directly, but rather a typeclass like
StrictOrderedSemiring
.
Equations
- MulPosStrictMono α = CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 < x2
Instances For
Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on
the left, namely a * b₁ < a * b₂ → b₁ < b₂
if 0 ≤ a
.
You should usually not use this very granular typeclass directly, but rather a typeclass like
LinearOrderedSemiring
.
Equations
- PosMulReflectLT α = ContravariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 < x2
Instances For
Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on
the right, namely a₁ * b < a₂ * b → a₁ < a₂
if 0 ≤ b
.
You should usually not use this very granular typeclass directly, but rather a typeclass like
LinearOrderedSemiring
.
Equations
- MulPosReflectLT α = ContravariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 < x2
Instances For
Typeclass for reverse monotonicity of multiplication by positive elements on the left,
namely a * b₁ ≤ a * b₂ → b₁ ≤ b₂
if 0 < a
.
You should usually not use this very granular typeclass directly, but rather a typeclass like
LinearOrderedSemiring
.
Equations
- PosMulReflectLE α = ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 ≤ x2
Instances For
Typeclass for reverse monotonicity of multiplication by positive elements on the right,
namely a₁ * b ≤ a₂ * b → a₁ ≤ a₂
if 0 < b
.
You should usually not use this very granular typeclass directly, but rather a typeclass like
LinearOrderedSemiring
.
Equations
- MulPosReflectLE α = ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 ≤ x2
Instances For
Alias of lt_of_mul_lt_mul_left
.
Alias of lt_of_mul_lt_mul_right
.
Alias of le_of_mul_le_mul_left
.
Alias of le_of_mul_le_mul_right
.
Alias of mul_le_mul_left
.
Alias of mul_le_mul_right
.
Alias of mul_lt_mul_left
.
Alias of mul_lt_mul_right
.
Alias of mul_le_mul_of_nonneg
.
Alias of mul_lt_mul_of_le_of_lt_of_pos_of_nonneg
.
Alias of mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
.
Alias of mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
.
Alias of mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
.
Alias of mul_lt_mul_of_lt_of_le_of_pos_of_nonneg
.
Alias of mul_lt_mul_of_lt_of_le_of_pos_of_nonneg
.
Alias of mul_lt_mul_of_pos
.
Alias of mul_lt_mul_of_pos'
.
Alias of mul_le_mul_of_nonneg'
.
Alias of mul_lt_mul_of_lt_of_le_of_pos_of_nonneg
.
Alias of mul_lt_mul_of_lt_of_le_of_pos_of_nonneg
.
Alias of mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
.
Alias of mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
.
Assumes left covariance.
Alias of Left.mul_pos
.
Assumes left covariance.
Assumes right covariance.
Assumes left covariance.
Alias of Left.mul_nonneg
.
Assumes left covariance.
Assumes right covariance.
Assumes left strict covariance.
Assumes right strict covariance.
Alias of Left.mul_lt_mul_of_nonneg
.
Assumes left strict covariance.
Alias of Left.mul_lt_mul_of_nonneg
.
Assumes left strict covariance.
Alias of Left.neg_of_mul_neg_right
.
Alias of Left.neg_of_mul_neg_left
.
Lemmas of the form a ≤ a * b ↔ 1 ≤ b
and a * b ≤ a ↔ b ≤ 1
,
which assume left covariance.
Lemmas of the form a ≤ b * a ↔ 1 ≤ b
and a * b ≤ b ↔ a ≤ 1
,
which assume right covariance.
Lemmas of the form 1 ≤ b → a ≤ a * b
.
Variants with < 0
and ≤ 0
instead of 0 <
and 0 ≤
appear in Mathlib/Algebra/Order/Ring/Defs
(which imports this file) as they need additional results which are not yet available here.
Lemmas of the form b ≤ c → a ≤ 1 → b * a ≤ c
.
Assumes left covariance.
Assumes left covariance.
Assumes left covariance.
Lemmas of the form b ≤ c → 1 ≤ a → b ≤ c * a
.
Assumes left covariance.
Assumes left covariance.
Assumes left covariance.
Lemmas of the form a ≤ 1 → b ≤ c → a * b ≤ c
.
Assumes right covariance.
Assumes right covariance.
Assumes right covariance.
Lemmas of the form 1 ≤ a → b ≤ c → b ≤ a * c
.
Assumes right covariance.
Assumes right covariance.
Assumes right covariance.
Assumes right covariance.
Alias of one_lt_mul_of_le_of_lt
.
bound
lemma for branching on 1 ≤ a ∨ a ≤ 1
when proving a ^ n ≤ a ^ m
The bound
tactic can't handle m ≠ 0
goals yet, so we express as 0 < m
See also pow_left_strictMono₀
and Nat.pow_left_strictMono
.
See also pow_right_strictMono'
.
See div_self
for the version with equality when a ≠ 0
.
Alias of the reverse direction of inv_pos
.
Alias of the reverse direction of inv_nonneg
.
Alias of zpow_pos
.
See le_inv_mul_iff₀'
for a version with multiplication on the other side.
See inv_mul_le_iff₀'
for a version with multiplication on the other side.
See inv_le_iff_one_le_mul₀
for a version with multiplication on the other side.
Alias of the reverse direction of one_le_inv₀
.
One direction of le_inv_mul_iff₀
where c
is allowed to be 0
(but b
must be nonnegative).
One direction of inv_mul_le_iff₀
where b
is allowed to be 0
(but c
must be nonnegative).
See le_mul_inv_iff₀'
for a version with multiplication on the other side.
See mul_inv_le_iff₀'
for a version with multiplication on the other side.
See le_div_iff₀'
for a version with multiplication on the other side.
See div_le_iff₀'
for a version with multiplication on the other side.
See inv_le_iff_one_le_mul₀'
for a version with multiplication on the other side.
One direction of le_mul_inv_iff₀
where c
is allowed to be 0
(but b
must be nonnegative).
One direction of mul_inv_le_iff₀
where b
is allowed to be 0
(but c
must be nonnegative).
One direction of le_div_iff₀
where c
is allowed to be 0
(but b
must be nonnegative).
One direction of div_le_iff₀
where b
is allowed to be 0
(but c
must be nonnegative).
Alias of le_div_iff₀
.
See le_div_iff₀'
for a version with multiplication on the other side.
Alias of div_le_iff₀
.
See div_le_iff₀'
for a version with multiplication on the other side.
See inv_anti₀
for the implication from right-to-left with one fewer assumption.
See also inv_le_of_inv_le₀
for a one-sided implication with one fewer assumption.
See also le_inv_of_le_inv₀
for a one-sided implication with one fewer assumption.
See lt_inv_mul_iff₀'
for a version with multiplication on the other side.
See inv_mul_lt_iff₀'
for a version with multiplication on the other side.
See inv_lt_iff_one_lt_mul₀
for a version with multiplication on the other side.
See lt_mul_inv_iff₀'
for a version with multiplication on the other side.
See mul_inv_lt_iff₀'
for a version with multiplication on the other side.
See lt_div_iff₀'
for a version with multiplication on the other side.
See div_lt_iff₀'
for a version with multiplication on the other side.
See inv_lt_iff_one_lt_mul₀'
for a version with multiplication on the other side.
See inv_strictAnti₀
for the implication from right-to-left with one fewer assumption.
See also inv_lt_of_inv_lt₀
for a one-sided implication with one fewer assumption.
See also lt_inv_of_lt_inv₀
for a one-sided implication with one fewer assumption.
Alias of inv_neg''
.
See le_inv_mul_iff₀
for a version with multiplication on the other side.
See inv_mul_le_iff₀
for a version with multiplication on the other side.
See le_mul_inv_iff₀
for a version with multiplication on the other side.
See mul_inv_le_iff₀
for a version with multiplication on the other side.
See le_div_iff₀
for a version with multiplication on the other side.
See div_le_iff₀
for a version with multiplication on the other side.
Alias of le_div_iff₀'
.
See le_div_iff₀
for a version with multiplication on the other side.
Alias of div_le_iff₀'
.
See div_le_iff₀
for a version with multiplication on the other side.
See lt_inv_mul_iff₀
for a version with multiplication on the other side.
See inv_mul_lt_iff₀
for a version with multiplication on the other side.
See lt_mul_inv_iff₀
for a version with multiplication on the other side.
See mul_inv_lt_iff₀
for a version with multiplication on the other side.
See lt_div_iff₀
for a version with multiplication on the other side.
See div_lt_iff₀
for a version with multiplication on the other side.