sum nonnegative iff elements nonnegative

Stream: Is there code for X?

[Eric Wieser]

Do we have anything like this?

import algebra.big_operators.order

variables {ι R : Type*} {Mᵢ : ι → Type*}

open_locale big_operators

lemma sum_nonneg_iff_forall_nonneg
  [fintype ι] [ordered_semiring R] [Π i, has_zero (Mᵢ i)]
  (f : Π i, Mᵢ i → R) (map_zero : ∀ x, f x 0 = 0) :
  (∀ (x : Π i, Mᵢ i), 0 ≤ ∑ i, f i (x i)) ↔ ∀ i (xi : Mᵢ i), 0 ≤ f i xi :=
begin
  split,
  { intros h i x,
    classical,
    convert h (pi.single i x) using 1,
    rw [finset.sum_eq_single_of_mem i (finset.mem_univ _) (λ j _ hji, _), pi.single_eq_same],
    rw [pi.single_eq_of_ne hji, map_zero], },
  { rintros h x,
    exact finset.sum_nonneg (λ i hi, h i (x i)), },
end

Maybe for dfinsupp or finsupp if not for pi?

[Johan Commelin]

what is docs#finset.sum_nonneg?

[Johan Commelin]

ah right, that gives you only one direction

[Johan Commelin]

I don't think we have this result

[Eric Wieser]

Can you think of a good name for it? The quantification over the pi type isn't something I've seen much of, and I don't know how to name that part