Zulip Chat Archive

Stream: new members

Topic: Un/currying if-then-else syntax


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

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

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 12:11):

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

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 12:12):

(PS we usually indent 2 spaces, not 4)

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

view this post on Zulip Javier Prieto (Dec 04 2020 at 12:18):

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

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

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

view this post on Zulip Kenny Lau (Dec 04 2020 at 12:22):

oh?

view this post on Zulip Eric Wieser (Dec 04 2020 at 12:23):

I have the same behavior

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

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