## Stream: new members

### Topic: Un/currying if-then-else syntax

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

I am trying to prove the following

import data.real.basic
import algebra.big_operators

open_locale big_operators  -- this enables the notation

universe x

variables
{ι : Type x} -- indexing type
[fintype ι] -- tell Lean that the set of all elements ι is finite.
[decidable_eq ι] -- and that its elements can be compared for equality

class rnd_var (X : ι → ℝ) :=
(probs_nonneg :  ∀ i, 0 ≤ X i)
(sum_probs_one : ∑ i, X i = 1)

lemma delta_if_det {X : ι → ℝ} [rnd_var X]
(h : ∀ i, X i = 0 ∨ X i = 1) :
(∃ j, ∀ i, if (i = j) then (X i = 1) else (X i = 0)) :=
begin
have h_ite : X = λ i, if (X i = 1) then 1 else 0,
{
-- curry the X using h somehow
sorry
},
have h_norm : ∑ i, X i = 1, {exact rnd_var.sum_probs_one,},
rw h_ite at h_norm,
have h_norm' : ∑ i, ite (X i = 1) 1 0 = 1,
{
-- how do I apply the lambda term to its argument?
sorry
},
-- split sum into two by value of X i
rw finset.sum_ite at h_norm',
have h_aux : ∑ (x : ι) in finset.filter (λ (x : ι), ¬X x = 1) finset.univ, 0 = 0,
{
-- one of the two sums is zero by sum_eq_zero
apply finset.sum_eq_zero,
tauto,
},
rw h_aux at h_norm',
norm_num at h_norm',
-- now h_norm' is essentially the goal but needs some massaging
sorry,
end


In words: if the probability mass function of a random variable only takes the values 0 and 1, then it's a Kronecker delta. I'm getting stuck trying to

• "Curry" the statement \forall i, X i = 0 \or X i = 1 into X = \lambda i, ite (X i = 1) 1 0
• Applying a lambda term i.e. showing (\lambda i, f i) i = f i

#### Kevin Buzzard (Dec 04 2020 at 12:10):

    have h_ite : X = λ i, if (X i = 1) then 1 else 0,
{
ext i,
split_ifs,
{ assumption },
{ cases h i,
{ assumption },
},
},


#### Kevin Buzzard (Dec 04 2020 at 12:11):

(\lambda i, f i) i = f i can be proved by refl

#### Kevin Buzzard (Dec 04 2020 at 12:12):

(PS we usually indent 2 spaces, not 4)

#### Kenny Lau (Dec 04 2020 at 12:17):

I've asked before why some people indent 4 spaces, and I think my conclusion is that they are not using the local VSCode Editor

#### Javier Prieto (Dec 04 2020 at 12:18):

Thank you, that was really helpful! I was missing the ext tactic.

#### Javier Prieto (Dec 04 2020 at 12:19):

I'm using VSCode, but I guess my global config says an indent is 4 spaces. Will change it locally if that's the preferred style in Lean.

#### Kevin Buzzard (Dec 04 2020 at 12:22):

@Kenny Lau whenever I start a new project I always have to change spaces from 4 to 2.

oh?

#### Eric Wieser (Dec 04 2020 at 12:23):

I have the same behavior

#### Kenny Lau (Dec 04 2020 at 12:34):

import data.real.basic
import algebra.big_operators

open_locale big_operators  -- this enables the notation

universe x

variables
{ι : Type x} -- indexing type
[fintype ι] -- tell Lean that the set of all elements ι is finite.
[decidable_eq ι] -- and that its elements can be compared for equality

class rnd_var (X : ι → ℝ) :=
(probs_nonneg :  ∀ i, 0 ≤ X i)
(sum_probs_one : ∑ i, X i = 1)

open finset

lemma delta_if_det {X : ι → ℝ} [rnd_var X]
(h : ∀ i, X i = 0 ∨ X i = 1) :
(∃ j, ∀ i, if (i = j) then (X i = 1) else (X i = 0)) :=
begin
have h_ite : X = λ i, if (X i = 1) then 1 else 0,
{ ext i,
cases h i with hxi0 hxi1,
{ rw [hxi0, if_neg (@zero_ne_one ℝ _ _)] },
{ rw [if_pos hxi1, hxi1] } },
have h_norm : ∑ i, X i = 1 := rnd_var.sum_probs_one,
rw h_ite at h_norm,
dsimp only at h_norm,
-- split sum into two by value of X i
rw sum_ite at h_norm,
have h_aux : (∑ x in univ.filter (λ x, ¬X x = 1), 0 : ℝ) = 0 := sum_const_zero,
rw h_aux at h_norm,
rw [add_zero, sum_const, nsmul_one, ← nat.cast_one, nat.cast_inj,
card_eq_one] at h_norm,
-- now h_norm is essentially the goal but needs some massaging
cases h_norm with j hj,
simp_rw [ext_iff, mem_filter, mem_univ, true_and, mem_singleton, nat.cast_one] at hj,
use j,
intro i,
rw if_congr_prop (hj i).symm iff.rfl iff.rfl,
cases h i with hxi0 hxi1,
{ rw [hxi0, if_neg (@zero_ne_one ℝ _ _)] },
{ rw [if_pos hxi1, hxi1] }
end


#### Javier Prieto (Dec 04 2020 at 13:11):

That works, thanks! So many lemmas I'm still not familiar with...

Last updated: May 11 2021 at 00:31 UTC