Zulip Chat Archive

Stream: new members

Topic: Finite sum of zeroes


view this post on Zulip 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!

view this post on Zulip Johan Commelin (Dec 03 2020 at 12:52):

@Javier Prieto It's called sum_eq_zero.

view this post on Zulip Johan Commelin (Dec 03 2020 at 12:53):

docs#finset.sum_eq_zero

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Dec 04 2020 at 08:08):

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

view this post on Zulip Johan Commelin (Dec 04 2020 at 08:08):

(It will be intros, apply hf)

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Reid Barton (Dec 07 2020 at 11:52):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Dec 07 2020 at 12:37):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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,

?

view this post on Zulip 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

view this post on Zulip Ruben Van de Velde (Dec 07 2020 at 13:25):

Oh, right, I misread

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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!

view this post on Zulip Bassem Safieldeen (Dec 07 2020 at 15:52):

Nice!


Last updated: May 15 2021 at 02:11 UTC