# Zulip Chat Archive

## 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):

#### 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):

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 (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

#### Ruben Van de Velde (Dec 07 2020 at 13:25):

Oh, right, I misread

#### 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