SMulPosMono for ENNReal

Stream: Is there code for X?

[Rémy Degenne]

I needed and proved SMulPosMono for ENNReal:

import Mathlib

open scoped ENNReal

instance ENNReal.instSMulPosMono : SMulPosMono ℕ ℝ≥0∞ := by
  constructor
  intro b _ n m hnm
  simp only [nsmul_eq_mul]
  gcongr

instance ENNReal.instPosSMulMono : PosSMulMono ℕ ℝ≥0∞ := by
  constructor
  intro b _ n m hnm
  simp only [nsmul_eq_mul]
  gcongr

However the SMulPosMono docstring tells me I should probably not prove it directly and it should follow from other classes. The question is: do you see something else I should prove about ENNReal that would imply that? ENNReal is not an OrderedSMul nor a SMulPosStrictMono because of infinity.

[Rémy Degenne]

@Yaël Dillies (pinged because you authored the SMulPosMono file)

[Yury G. Kudryashov]

IMHO, we should have instances for Nat and Int that assume monotonicity of addition and nothing more.

[Yaël Dillies]

I think what you're doing is correct, Rémy.

[Yaël Dillies]

I purposely wrote a somewhat aggressive docstring to make sure we don't accidentally settle on a wrong design decision too quickly, but here this looks fine.

[Rémy Degenne]

I agree with Yury that a proof for much more general types is possible, but I don't know the classes related to order and operations.
My proof above generalizes to the following, but there should be no need for a multiplication:

instance {α : Type*} [OrderedSemiring α] [CharZero α] : SMulPosMono ℕ α := by
  constructor
  intro b hb n m hnm
  simp only [nsmul_eq_mul]
  gcongr

Should I use something like [CovariantClass α α (· + · ) (· ≤ ·)]?

[Rémy Degenne]

That works:

instance {α : Type*} [AddMonoid α] [Preorder α]
    [CovariantClass α α (· + ·) (· ≤ ·)]
    [CovariantClass α α (Function.swap (· + ·)) (· ≤ ·)] :
    SMulPosMono ℕ α := by
  constructor
  intro b hb n m hnm
  induction m with
  | zero =>
    simp only [Nat.zero_eq, nonpos_iff_eq_zero] at hnm
    simp only [hnm, zero_smul, Nat.zero_eq, le_refl]
  | succ m ih =>
    cases hnm with
    | refl => exact le_rfl
    | step hnm =>
      refine (ih hnm).trans ?_
      have h := AddMonoid.nsmul_succ m b
      simp only [nsmul_eq_smul] at h
      rw [Nat.succ_eq_add_one, h]
      conv_lhs => rw [← zero_add (m • b)]
      exact add_le_add hb le_rfl

[Yaël Dillies]

Might as well use OrderedAddCommMonoid

[Yury G. Kudryashov]

I think that either one of CovariantClass assumptions should be enough but I'm on a phone now, so can't test.

[Rémy Degenne]

You're right, I can remove one of the two CovariantClass if I replace add_le_add by add_le_add_right on the last line.