induction over fold

Stream: new members

[Marcus Rossel]

I want to prove the following:

example {n : ℕ} {v : fin n → ℝ} : 0 ≤ finset.univ.fold (+) 0 (λ i, (v i) ^ 2) :=
  sorry

The inequality obviously holds for the initial value 0, and since every additional term adds a non-negative value, the inequality will continue to hold. I don't know what lemma to use to communicate this to Lean though.
Any hints would be appreciated. Thanks

[Eric Rodriguez]

does induction n generalizing v help?

[Eric Rodriguez]

O guess you'll also need some of docs#fin.cast_succ and family

[Yaël Dillies]

Any reason you're not using docs#finset.sum?

[Patrick Johnson]

You can generalize finset.univ

import data.real.basic

example {n : ℕ} {v : fin n → ℝ} :
  0 ≤ finset.univ.fold (+) 0 (λ i, (v i) ^ 2) :=
begin
  generalize : finset.univ = s,
  apply s.induction_on; clear s,
  { refl },
  { rintro k s h₁ h₂,
    rw finset.fold_insert h₁,
    exact add_nonneg (sq_nonneg _) h₂ },
end

[Patrick Johnson]

The sum version:

import data.real.basic
open_locale big_operators

example {n : ℕ} {v : fin n → ℝ} : 0 ≤ ∑ i in finset.univ, (v i) ^ 2 :=
finset.sum_nonneg (λ _ _, sq_nonneg _)

[Patrick Johnson]

Just realized they are defeq:

example {n : ℕ} {v : fin n → ℝ} : 0 ≤ finset.univ.fold (+) 0 (λ i, (v i) ^ 2) :=
finset.sum_nonneg (λ _ _, sq_nonneg _)