monotonicity for sums and products of monotone functions

Stream: Is there code for X?

[Damiano Testa]

Dear All,

are the lemmas below in mathlib? I thought that they would be already available, but I could not find them!

Thanks!

[In case you are wondering, I want to use them to prove that polynomials over ℕ are monotone and, if non-constant, strict_mono.]

import data.pi
import algebra.ordered_monoid_lemmas

variables {X Y : Type*}

/--  The product of two monotone functions is monotone. -/
@[to_additive "The sum of two monotone functions is monotone."]
lemma monotone_mul_of_monotone_of_monotone [preorder X] [has_mul Y] [preorder Y]
  [covariant_class Y Y (*) (≤)] [covariant_class Y Y (function.swap (*)) (≤)]
  {f g : X → Y} (hf : monotone f) (hg : monotone g) :
  monotone (f * g)
| a b ab := calc  (f * g) a ≤ f a * g b : mul_le_mul_left' (hg ab) _
                        ... ≤ f b * g b : mul_le_mul_right' (hf ab) _

/--  The product of two strictly monotone functions is strictly monotone. -/
@[to_additive
"The sum of two strictly monotone functions is strictly monotone."]
lemma strict_mono_mul_of_strict_mono_of_strict_mono [has_lt X] [has_mul Y] [preorder Y]
  [covariant_class Y Y (*) (<)] [covariant_class Y Y (function.swap (*)) (<)]
  {f g : X → Y} (hf : strict_mono f) (hg : strict_mono g) :
  strict_mono (f * g)
| a b ab := calc  (f * g) a < f a * g b : mul_lt_mul_left' (hg ab) _
                        ... < f b * g b : mul_lt_mul_right' (hf ab) _

/--  The product of a monotone function and a strictly monotone function is strictly monotone. -/
@[to_additive
"The sum of a monotone function and a strictly monotone function is strictly monotone."]
lemma strict_mono_mul_of_mono_of_strict_mono [preorder X] [preorder Y] [has_mul Y] {f g : X → Y}
  [covariant_class Y Y (*) (<)] [covariant_class Y Y (function.swap (*)) (≤)]
  (hf : monotone f) (hg : strict_mono g) :
  strict_mono (f * g)
| a b ab := calc  (f * g) a < f a * g b : mul_lt_mul_left' (hg ab) _
                        ... ≤ f b * g b : mul_le_mul_right' (hf ab.le) _

/--  The product of a strictly monotone function and a monotone function is strictly monotone. -/
@[to_additive
"The sum of a strictly monotone function and a monotone function is strictly monotone."]
lemma strict_mono.mul_of_strict_mono_of_mono [preorder X] [preorder Y] [has_mul Y] {f g : X → Y}
  [covariant_class Y Y (*) (≤)] [covariant_class Y Y (function.swap (*)) (<)]
  (hf : strict_mono f) (hg : monotone g) :
  strict_mono (f * g)
| a b ab := calc  (f * g) a ≤ f a * g b : mul_le_mul_left' (hg ab.le) _
                        ... < f b * g b : mul_lt_mul_right' (hf ab) _

[Yakov Pechersky]

If they don't exist, I'd name them monotone.mul, strict_mono.mul, etc

[Yakov Pechersky]

The last one would be strict_mono.mul, since it is stronger

[Damiano Testa]

Thanks Yakov! By the magic of the naming convention, you almost found the lemmas in mathlib! The lemma called monotone.mul is

monotone.mul :
  ∀ {α : Type u_3} {β : Type u_4} [_inst_1 : linear_ordered_semiring α] [_inst_2 : preorder β]
 {f g : β → α},
    monotone f →
    monotone g →
    (∀ (x : β), 0 ≤ f x) →
    (∀ (x : β), 0 ≤ g x) →
    monotone (λ (x : β), f x * g x)

[Eric Wieser]

That's just because that lemma predates your order refactor, right?

[Damiano Testa]

I can see that monotone.mul is likely a common form to in which this lemma is applied, but the assumptions imply an addition which seems to play no role.

[Damiano Testa]

Yes, this lemma has not been changed (yet) by the refactor: I have taken a break, but I am planning to continue with the refactor soon.

[Damiano Testa]

Ok, the first lemma (at least) is in mathlib: it is called monotone.mul'!

[Damiano Testa]

Why does library_search not find the lemma, though?

lemma monotone.mul_new [preorder X] [has_mul Y] [preorder Y]
  [covariant_class Y Y (*) (≤)] [covariant_class Y Y (function.swap (*)) (≤)]
  {f g : X → Y} (hf : monotone f) (hg : monotone g) :
  monotone (f * g) :=
begin
--  library_search : `library_search` failed.
  exact monotone.mul' hf hg -- works
end

#check @monotone.mul'
/-
monotone.mul' :
  ∀ {α : Type u_3} [_inst_1 : has_mul α] {β : Type u_4} {f g : β → α} [_inst_2 : preorder α]
  [_inst_3 : preorder β] [_inst_4 : covariant_class α α has_mul.mul has_le.le]
  [_inst_5 : covariant_class α α (function.swap has_mul.mul) has_le.le],
    monotone f → monotone g → monotone (λ (x : β), f x * g x)
-/

[Mario Carneiro]

Most of these should definitely exist without the monotone part, under names like mul_le_mul

[Mario Carneiro]

in particular, you don't need those calc proofs

[Eric Wieser]

Library search doesn't know to rewrite through docs#pi.mul_def

[Damiano Testa]

Ah, thanks Eric!

Mario, does your comment mean that these lemmas should not be in mathlib in this form, or they should, but their proofs should use their non-monotone lemma?

[Eric Wieser]

I think the latter

[Mario Carneiro]

I don't see anything wrong with the lemmas as stated, but the proofs can be shorter. If there is a monotone lemma already then use that, otherwise use the mul_le_mul type lemma

[Damiano Testa]

#8465.

The conclusion seems to be that all except for one of the lemmas were already in mathlib. I added the missing one and also I added doc-strings to the four lemmas.

[The missing lemma was the one about the product of strictly monotone functions.]