Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-08 09:14 f5a600f8

View on Github →

feat(algebra/order/ring): Non-cancellative ordered semirings (#16172)

Historical background

This tackles a problem that we have had for six years (#2697 for its move to mathlib, before it was in core): ordered_semiring assumes that addition and multiplication are strictly monotone. This led to weirdness within the algebraic order hierarchy:

  • ennreal/ereal/enat needed custom lemmas (∞ + 0 = ∞ = ∞ + 1, 1 * ∞ = ∞ = 2 * ∞).
  • A canonically_ordered_comm_semiring was not an ordered_comm_semiring!

What this PR does

This PR solves the problem minimally by renaming ordered_(comm_)semiring to strict_ordered_(comm_)semiring and adding a new class ordered_(comm_)semiring that doesn't assume strict monotonicity of addition and multiplication but only monotonicity:

class ordered_semiring (α : Type*) extends semiring α, ordered_add_comm_monoid α :=
(zero_le_one : (0 : α) ≤ 1)
(mul_le_mul_of_nonneg_left  : ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b)
(mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c)
class ordered_comm_semiring (α : Type*) extends ordered_semiring α, comm_semiring α
class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_nonneg : ∀ a b : α, 0 ≤ a → 0 ≤ b → 0 ≤ a * b)
class ordered_comm_ring (α : Type u) extends ordered_ring α, comm_ring α
class strict_ordered_semiring (α : Type*) extends semiring α, ordered_cancel_add_comm_monoid α :=
(zero_le_one : (0 : α) ≤ 1)
(mul_lt_mul_of_pos_left  : ∀ a b c : α, a < b → 0 < c → c * a < c * b)
(mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c)
class strict_ordered_comm_semiring (α : Type*) extends strict_ordered_semiring α, comm_semiring α
class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_pos     : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)
class strict_ordered_comm_ring (α : Type*) extends strict_ordered_ring α, comm_ring α

Whatever happened to the decidable lemmas?

Scrolling through the diff, you will see that only one lemma in the decidable namespace out of many survives this PR. Those lemmas were originally meant to avoid using choice in the proof of nat and int lemmas. The need for decidability originated from the proofs of mul_le_mul_of_nonneg_left/mul_le_mul_of_nonneg_right.

protected lemma decidable.mul_le_mul_of_nonneg_left [@decidable_rel α (≤)]
  (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b :=
begin
  by_cases ba : b ≤ a, { simp [ba.antisymm h₁] },
  by_cases c0 : c ≤ 0, { simp [c0.antisymm h₂] },
  exact (mul_lt_mul_of_pos_left (h₁.lt_of_not_le ba) (h₂.lt_of_not_le c0)).le,
end

Now that these are fields to ordered_semiring, they are already choice-free. Instead, choice is now used in showing that an ordered_cancel_semiring is an ordered_semiring.

@[priority 100] -- see Note [lower instance priority]
instance ordered_cancel_semiring.to_ordered_semiring : ordered_semiring α :=
{ mul_le_mul_of_nonneg_left := λ a b c hab hc, begin
    obtain rfl | hab := hab.eq_or_lt,
    { refl },
    obtain rfl | hc := hc.eq_or_lt,
    { simp },
    { exact (mul_lt_mul_of_pos_left hab hc).le }
  end,
  mul_le_mul_of_nonneg_right := λ a b c hab hc, begin
    obtain rfl | hab := hab.eq_or_lt,
    { refl },
    obtain rfl | hc := hc.eq_or_lt,
    { simp },
    { exact (mul_lt_mul_of_pos_right hab hc).le }
  end,
  ..‹ordered_cancel_semiring α› }

It seems unreasonable to make that instance depend on @decidable_rel α (≤) even though it's only needed for the proofs.

Other changes

To have some lemmas in the generality of the new ordered_semiring, I needed a few new lemmas:

  • bit0_mono
  • bit0_strict_mono It was also simpler to golf analysis.special_functions.stirling using positivity rather than fixing it so I introduce the following (simple) positivity extensions:
  • positivity_succ
  • positivity_factorial
  • positivity_asc_factorial

Estimated changes

added theorem geom_sum_ne_zero
modified theorem geom_sum_neg_iff
added theorem geom_sum_pos'
modified theorem geom_sum_pos
modified theorem geom_sum_pos_and_lt_one
modified theorem geom_sum_pos_iff
modified theorem one_lt_pow
modified theorem pow_lt_one
modified theorem sq_pos_of_neg
modified theorem add_le_mul_two_add
added theorem antitone.const_mul
added theorem antitone.mul
added theorem antitone.mul_const
added theorem antitone.mul_monotone
added theorem bit1_mono
modified theorem bit1_pos'
modified theorem cmp_mul_pos_left
modified theorem cmp_mul_pos_right
deleted theorem decidable.monotone_mul
deleted theorem decidable.strict_mono_mul
modified theorem four_ne_zero
deleted theorem gt_of_mul_lt_mul_neg_left
modified theorem lt_add_one
added theorem lt_mul_left
added theorem lt_mul_right
modified theorem lt_one_add
modified theorem lt_two_mul_self
modified theorem monotone.const_mul
modified theorem monotone.mul
added theorem monotone.mul_antitone
modified theorem monotone.mul_const
modified theorem monotone.mul_strict_mono
modified theorem monotone_mul_left_of_nonneg
modified theorem mul_le_mul_of_nonpos_left
modified theorem mul_le_mul_of_nonpos_right
modified theorem mul_le_one
modified theorem mul_lt_mul'
modified theorem mul_lt_mul
modified theorem mul_lt_mul_of_neg_left
modified theorem mul_lt_mul_of_neg_right
deleted theorem mul_self_le_mul_self
modified theorem nat.strict_mono_cast
deleted theorem one_lt_mul
modified theorem one_lt_mul_of_le_of_lt
modified theorem one_lt_mul_of_lt_of_le
modified theorem one_lt_two
deleted theorem ordered_ring.mul_nonneg
modified theorem pow_nonneg
added theorem strict_anti.const_mul
added theorem strict_anti.mul_const
modified theorem strict_mono.mul
modified theorem strict_mono.mul_monotone
modified theorem three_ne_zero
modified theorem two_ne_zero
added theorem zero_lt_four'
modified theorem zero_lt_four
modified theorem zero_lt_one'
modified theorem zero_lt_one
added theorem zero_lt_three'
modified theorem zero_lt_three
added theorem zero_lt_two'
modified theorem zero_lt_two
modified theorem filter.germ.coe_le
added theorem filter.germ.coe_nonneg
modified theorem filter.germ.coe_pow
modified theorem filter.germ.coe_smul'
modified theorem filter.germ.coe_smul
deleted theorem filter.germ.coe_zpow
modified theorem filter.germ.const_bot
added theorem filter.germ.const_div
deleted theorem filter.germ.const_inf
added theorem filter.germ.const_inv
modified theorem filter.germ.const_le
added theorem filter.germ.const_pow
added theorem filter.germ.const_smul
deleted theorem filter.germ.const_sup
modified theorem filter.germ.const_top