Un/currying if-then-else syntax

Stream: new members

[Javier Prieto]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(PS we usually indent 2 spaces, not 4)

[Kenny Lau]

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]

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

[Javier Prieto]

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]

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

[Kenny Lau]

oh?

[Eric Wieser]

I have the same behavior

[Kenny Lau]

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]

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