Finite sum of zeroes

Stream: new members

[Javier Prieto]

Hi everyone. I'm very new to Lean, so this is a very basic question. I want to show that the constant function f : i -> R where i is a finite type and f i = 0 everywhere integrates to zero. Here is my code:

import data.real.basic
import algebra.big_operators

open finset
open_locale big_operators

universe x

variables {ι : Type x} [fintype ι]
variables {f : ι → ℝ}

lemma
sum_of_zero_eq_zero (f : ι → ℝ) : ∀ i, f i = 0 → ∑ i, f i = 0 :=
begin
    sorry
end

I've been trying to find this lemma in the library for a while and failing, but it has to be there somewhere right? My proof attempts have also been unsuccessful so far. Thanks in advance!

[Johan Commelin]

@Javier Prieto It's called sum_eq_zero.

[Johan Commelin]

docs#finset.sum_eq_zero

[Javier Prieto]

Thank you for your answer @Johan Commelin . I think that's the result I need. However, when I try to use it in (a slightly modified version of) my lemma above like:

lemma
sum_of_zero_eq_zero (f : ι → ℝ) (hf : ∀ i, f i = 0) : ∑ i, f i = 0 :=
begin
    apply sum_eq_zero hf,
end

I get the following type error:

type mismatch at application
  sum_eq_zero hf
term
  hf
has type
  ∀ (i : ι), f i = 0
but is expected to have type
  ∀ (x : ?m_1), x ∈ ?m_2 → ?m_4 x = 0

My guess is that because sum_eq_zero is defined for finite sets but my ι is a finite type with no notion of membership ∈, I'd need to either redefine ι as a finset or find a similar result for fintype. Am I too far off the mark?

[Johan Commelin]

@Javier Prieto Just write apply sum_eq_zero, and prove the resulting goal afterwords.

[Johan Commelin]

(It will be intros, apply hf)

[Javier Prieto]

Yeah, that worked. I still need to wrap my head around the syntax of apply. Thank you so much!

[Javier Prieto]

Re-using this thread to kindly ask about the converse

lemma sum_nonneg_zero {f : ι → ℝ} (hf1 : ∑ i, f i = 0) (hf2: ∀ i, 0 ≤ f i) :
∀ i, f i = 0 :=
begin
  intros i,
  specialize hf2 i,
  replace hf2 := le_iff_lt_or_eq.mp hf2,
  cases hf2 with fi_pos fi_zero, -- split into f i > 0 and f i = 0
  exfalso, -- sum of positive reals cannot be zero
  sorry,
  rwa fi_zero,
end

I have no problem showing this for the sum of two positive real numbers, so I was thinking I could use induction, but maybe that's overkill?

[Reid Barton]

I think you're looking for docs#finset.sum_eq_zero_iff_of_nonneg

[Javier Prieto]

Indeed, thank you. I'm still having trouble applying it though. When I try the following

lemma sum_nonneg_zero {f : ι → ℝ} : (∀ i, 0 ≤ f i) → (∑ i, f i = 0 ↔ ∀ i, f i = 0) :=
begin
  apply sum_eq_zero_iff_of_nonneg,
end

the tactic "fails to unify" even though that worked for sum_eq_zero and they look the same to my untrained eye.

[Reid Barton]

It's not exactly the same because there is this s in the finset lemma.

[Reid Barton]

The sum is defined as the sum over finset.univ but ∀ i isn't defined as for all i in finset.univ.

[Javier Prieto]

Yes, but that s was also present in the sum_eq_zero lemma and this syntax worked in that case (still unsure why to be honest). That's what confuses me.

[Reid Barton]

apply foo matches the conclusion of foo with the goal. In the example where apply sum_eq_zero worked, you only had ∑ i, f i = 0 in the goal. Here, the goal also includes these ∀ i, 0 ≤ f i, ∀ i, f i = 0 bits which have the wrong shape.

[Ruben Van de Velde]

Does it work if you do

intro h,
apply sum_eq_zero_iff_of_nonneg,

?

[Reid Barton]

It shouldn't work because there is still ∀ i, f i = 0 in the conclusion to deal with

[Ruben Van de Velde]

Oh, right, I misread

[Bassem Safieldeen]

lemma sum_nonneg_zero {f : ι → ℝ} (hf1 : ∑ i, f i = 0) (hf2: ∀ i, 0 ≤ f i) :
∀ i, f i = 0 :=
begin
  intro i,
  have H : ∑ i, f i = 0 ↔ ∀ i, f i = 0, {
    rw sum_eq_zero_iff_of_nonneg,
    {
      finish,
    },
    {
      simp only [hf2],
      finish,
    },
  },
  have H2 : ∀ i, f i = 0, {
    exact H.1 hf1,
  },
  apply H2,
end

[Ruben Van de Velde]

Right, but note that the original question was an iff, and you only proved one direction. (Though the other one should be fairly simple.)

[Javier Prieto]

Here's the proof with the iff

lemma sum_nonneg_zero' {f : ι → ℝ} : (∀ i, 0 ≤ f i) → (∑ i, f i = 0 ↔
∀ i, f i = 0) :=
begin
  intro hs,
  rw sum_eq_zero_iff_of_nonneg,
  finish,
  finish,
end

Very easy indeed!

[Bassem Safieldeen]

Nice!