mul_sup for non-negative reals

Stream: Is there code for X?

[Moritz Doll]

I found a version of mul_sup for nnreal, but not for real, is there an easy way to get it for non-negative real?

[Patrick Johnson]

Adapted from nnreal.mul_sup:

lemma mul_sup {a b c : ℝ} (h₁ : 0 ≤ a) : a * (b ⊔ c) = (a * b) ⊔ (a * c) :=
begin
  cases le_total b c with h h,
  { simp [sup_eq_max, max_eq_right h, max_eq_right (mul_le_mul_of_nonneg_left h h₁)] },
  { simp [sup_eq_max, max_eq_left h, max_eq_left (mul_le_mul_of_nonneg_left h h₁)] },
end

[Patrick Johnson]

Maybe there is already a similar lemma in mathlib, but I can't find it.

[Yaël Dillies]

Also, file#data/real/pointwise for Sup instead of sup

[Eric Wieser]

Presumably this should actually be stated about max?

[Yaël Dillies]

Not the most general version of the lemma

[Eric Wieser]

What makes that any more / less general?

[Yaël Dillies]

sup is more general than max, so the max statement is a one-liner from the one for sup.

[Yaël Dillies]

Of course, over an arbitrary type, not just $\R$

[Eric Wieser]

We don't have a typeclass to express this over an arbitrary type though? Or do we?

[Yaël Dillies]

Surely we do, after all we have docs#mul_sup

[Yaël Dillies]

Just take ordered_semiring as in docs#mul_le_mul_of_nonneg_left and Patrick's proof goes through.

[Eric Wieser]

Well the ennreal one is docs#ennreal.max_mul

[Yaël Dillies]

Nuke that lemma!

[Eric Wieser]

I'm not really sure what you're describing above without a code sample, but I assume you're not at lean right now

[Yaël Dillies]

Okay, the sup statement is hard to get because lattice groups are so baby in mathlib.

[Yaël Dillies]

import algebra.order.ring

variables {α : Type*} [linear_ordered_semiring α]

@[simp] lemma max_mul (a b c : α) (hc : 0 ≤ c) : max (c * a) (c * b) = c * max a b :=
begin
  obtain h | h := le_total a b,
  { rw [max_eq_right (mul_le_mul_of_nonneg_left h hc), max_eq_right h] },
  { rw [max_eq_left (mul_le_mul_of_nonneg_left h hc), max_eq_left h] }
end