Zulip Chat Archive

Stream: new members

Topic: Splitting sum with dite


view this post on Zulip Yakov Pechersky (Jul 29 2020 at 17:16):

What's the lemma/definition that can break a sum into the cases that are relevant to the internal ite or dite? My current goal state is:

R : Type u_1,
_inst_1 : field R,
n : ,
i j : fin (n + 2),
h : i  j,
A : matrix (fin (n + 2)) (fin (n + 2)) R,
ix jx : fin (n + 2),
hj : jx = j,
hi : ¬jx = i
  (x : fin (n + 2)),
      dite (x = j) (λ (h : x = j), ite (ix = i) 1 0)
          (λ (h : ¬x = j), dite (x = i) (λ (h : x = i), ite (ix = j) 1 0) (λ (h : ¬x = i), ite (ix = x) 1 0)) *
        A x j =
    A ix i

view this post on Zulip Yakov Pechersky (Jul 29 2020 at 17:18):

The statement being proved is wrong in general (I was left-multiplying by the swap-column matrix instead of right-multiplying), but the question stands.

view this post on Zulip Mario Carneiro (Jul 29 2020 at 17:33):

You can usually use split_ifs if you have an ite in the goal, but here it won't work because it's under a binder

view this post on Zulip Mario Carneiro (Jul 29 2020 at 17:33):

first you have to figure out what you want to do about the sum

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 03:50):

See docs#finset.prod_apply_dite


Last updated: May 17 2021 at 23:14 UTC