Zulip Chat Archive

Stream: Is there code for X?

Topic: finset.sup_mul_left

Scott Morrison (Feb 28 2022 at 06:55):

Do we have

theorem finset.sup_mul_left
  {ι : Type*} (s : finset ι) (f : ι → nnreal) (a : nnreal) :
  s.sup (λ i, a * f i) = a * s.sup f :=
sorry

(or similarly for appropriate generalisations away from nnreal)?

Johan Commelin (Feb 28 2022 at 06:58):

lemma mul_finset_sup {α} {f : α → ℚ≥0} {s : finset α} (r : ℚ≥0) :
  r * s.sup f = s.sup (λa, r * f a) :=
begin
  refine s.induction_on _ _,
  { simp [bot_eq_zero] },
  { assume a s has ih, simp [has, ih, mul_sup], }
end

exists in LTE. Not sure if that is helpful...

Scott Morrison (Feb 28 2022 at 07:23):

I see, so you've done another special case. :-) If anyone can think of a good generalisation, let me know!

Johan Commelin (Feb 28 2022 at 07:55):

cc @Damiano Testa

Damiano Testa (Feb 28 2022 at 07:55):

I am trying to see what can be done using the new pos_mul typeclasses. I will report soon!

Alistair Tucker (Feb 28 2022 at 08:27):

Do you know about comp_sup_eq_sup_comp_of_is_total?

Damiano Testa (Feb 28 2022 at 08:41):

I think that what Alistair suggests is probably a better way. At least before the new pos_mul typeclasses advance more. If you want to see a not-so-pretty way of obtaining the results above, below is some not polished code!

import algebra.order.monoid_lemmas_zero_lt
import data.real.nnreal


open_locale nnreal classical
open zero_lt finset finsupp

lemma new.mul_sup {α : Type*} [mul_zero_class α] [linear_order α] [pos_mul_mono α]
  {a b c : α} (a0 : 0 < a) : a * (b ⊔ c) = a * b ⊔ a * c :=
begin
  cases le_total b c with h h,
  { rw [sup_eq_max, sup_eq_max, max_eq_right h, max_eq_right],
    exact @covariant_class.elim {z : α // 0 < z} α (λ x y, x * y) (≤) _ ⟨a, a0⟩ _ _ h },
  { rw [sup_eq_max, sup_eq_max, max_eq_left h, max_eq_left],
    exact @covariant_class.elim {z : α // 0 < z} α (λ x y, x * y) (≤) _ ⟨a, a0⟩ _ _ h }
end

theorem new.finset.sup_mul_left {α : Type*} [mul_zero_class α] [linear_order α] [pos_mul_mono α]
  [order_bot α] (b0 : (⊥ : α) = 0)
  {ι : Type*} (s : finset ι) (f : ι → α) (a : α) :
  s.sup (λ i, a * f i) = a * s.sup f :=
begin
  refine s.induction_on _ _,
  { simp only [sup_empty, b0, mul_zero] },
  { by_cases a0 : a = ⊥,
    { simp [a0, b0] },
    { assume b s hbs ih,
      have : 0 < a, { rw ← b0, exact lt_of_le_of_ne bot_le (ne.symm a0) },
      simp [ih, sup_insert, new.mul_sup this] } }
end

instance : pos_mul_mono ℝ≥0 :=
{ elim := λ a0 b c bc, mul_le_mul_of_nonneg_left bc a0.2.le }

theorem finset.sup_mul_left
  {ι : Type*} (s : finset ι) (f : ι → nnreal) (a : nnreal) :
  s.sup (λ i, a * f i) = a * s.sup f :=
new.finset.sup_mul_left nnreal.bot_eq_zero _ _ _

Damiano Testa (Feb 28 2022 at 08:42):

However, for this to be viable, there is the need of some API for pos_mul, which I have not yet gotten around to.

Yaël Dillies (Feb 28 2022 at 10:52):

Have a look at file#data/real/pointwise

Eric Wieser (Feb 28 2022 at 12:26):

Does this follow from docs#order_iso.map_finset_sup?

Eric Wieser (Feb 28 2022 at 12:27):

... if that existed

Eric Wieser (Feb 28 2022 at 12:39):

(finset.comp_sup_eq_sup_comp _ _ _).symm is very close to a proof. My orange bars aren't behavior so I can't tell you more than tat

Eric Wieser (Feb 28 2022 at 12:44):

theorem nnreal.finset_sup_mul_left
  {ι : Type*} (s : finset ι) (f : ι → nnreal) (a : nnreal) :
  s.sup (λ i, a * f i) = a * s.sup f :=
(finset.comp_sup_eq_sup_comp _ (nnreal.mul_sup a) (mul_zero a)).symm