## Stream: new members

### Topic: Finite sum of zeroes

#### Javier Prieto (Dec 03 2020 at 12:45):

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 (Dec 03 2020 at 12:52):

@Javier Prieto It's called sum_eq_zero.

#### Johan Commelin (Dec 03 2020 at 12:53):

docs#finset.sum_eq_zero

#### Javier Prieto (Dec 04 2020 at 08:02):

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 (Dec 04 2020 at 08:08):

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

#### Johan Commelin (Dec 04 2020 at 08:08):

(It will be intros, apply hf)

#### Javier Prieto (Dec 04 2020 at 08:15):

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

#### Javier Prieto (Dec 07 2020 at 11:41):

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 (Dec 07 2020 at 11:52):

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

#### Javier Prieto (Dec 07 2020 at 12:34):

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 (Dec 07 2020 at 12:37):

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

#### Reid Barton (Dec 07 2020 at 12:38):

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

#### Javier Prieto (Dec 07 2020 at 12:45):

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 (Dec 07 2020 at 13:01):

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 (Dec 07 2020 at 13:06):

Does it work if you do

intro h,
apply sum_eq_zero_iff_of_nonneg,


?

#### Reid Barton (Dec 07 2020 at 13:12):

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

#### Bassem Safieldeen (Dec 07 2020 at 15:21):

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 (Dec 07 2020 at 15:33):

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 (Dec 07 2020 at 15:49):

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 (Dec 07 2020 at 15:52):

Nice!

Last updated: May 15 2021 at 02:11 UTC